Ignore:
Timestamp:
Feb 14, 2013, 7:10:23 PM (8 years ago)
Author:
garnier
Message:

Clight to Cminor, statements: some cases down. Subset of the simulation relation defined and seems to work.
Some cosmetic changes in toCminorCorrectnessExpr in order to clarify things in toCminorCorrectness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Clight_abstract.ma

    r2601 r2667  
    4747definition cl_eval_expr ≝ eval_expr.
    4848
     49(* creating aliases constructors for states and continuations *)
    4950definition ClState ≝ State.
     51
     52definition ClKseq ≝ Kseq.
Note: See TracChangeset for help on using the changeset viewer.