Changeset 1233 for src/RTL/semantics.ma


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (8 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1141 r1233  
    264264     [ nil ⇒ Some ? (smerge2 v)
    265265     | _ ⇒ None ? ]].
    266 
     266(*
    267267definition RTL_exec : execstep io_out io_in ≝
    268268  mk_execstep … ? is_final mem_of_state eval_statement.
    269 
     269*)
    270270(* CSC: XXX the program type does not fit with the globalenv and init_mem
    271271definition make_initial_state : rtl_program → res (genv × state) ≝
Note: See TracChangeset for help on using the changeset viewer.