Changeset 1601 for src/LIN


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1379 r1601  
    11include "LIN/joint_LTL_LIN.ma".
    2 include "utilities/lists.ma".
     2include "basics/lists/list.ma".
    33
    44definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
  • src/LIN/semantics.ma

    r1451 r1601  
    2727        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
    2828     (joint_if_code … (lin_params …) fn)) ;
    29   OK … (inject … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
     29  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    3030// qed.
    3131
Note: See TracChangeset for help on using the changeset viewer.