Ignore:
Timestamp:
Mar 28, 2013, 2:59:43 PM (8 years ago)
Author:
campbell
Message:

Sketch out how Cminor to RTLabs correctness would fit into the
front-end measurable traces proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_abstract.ma

    r2737 r3007  
    4242definition CmCallstate ≝ Callstate.
    4343
     44lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall.
     45* #a try #b try #c try #d try #e try #f try #g try #h try #i try #j
     46normalize % #E destruct
     47qed.
Note: See TracChangeset for help on using the changeset viewer.