Changeset 2496 for src/Cminor


Ignore:
Timestamp:
Nov 27, 2012, 5:50:51 PM (7 years ago)
Author:
garnier
Message:

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/abstract.ma

    r2489 r2496  
    2727| Finalstate _ ⇒ cl_other
    2828].
     29
     30definition cm_genv ≝ genv.
     31
     32definition cm_env ≝ env.
     33
     34definition cm_cont ≝ cont.
     35
     36definition cm_eval_expr ≝ eval_expr.
     37
Note: See TracChangeset for help on using the changeset viewer.