Changeset 1244 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Sep 21, 2011, 6:08:50 PM (9 years ago)
Author:
campbell
Message:

Sort out Clight semantics equivalence proof for new SmallstepExec?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1231 r1244  
    499499axiom MainMissing : String.
    500500
    501 let rec make_global (p:clight_program) : genv ≝
    502   globalenv Genv ?? (fst ??) p.
     501definition make_global : clight_program → genv ≝
     502λp. globalenv Genv ?? (fst ??) p.
    503503
    504504let rec make_initial_state (p:clight_program) : res state ≝
Note: See TracChangeset for help on using the changeset viewer.