Changeset 1301


Ignore:
Timestamp:
Oct 5, 2011, 11:35:35 PM (8 years ago)
Author:
sacerdot
Message:

Axioms re-grouped according to their use.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1300 r1301  
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1010
     11(*CSC: XXXXX *)
     12axiom rtl_init_locals : list register → register_env beval.
    1113axiom rtl_pop_frame: unit → res unit.
    1214axiom rtl_save_frame: unit → register_env beval → unit.
     
    2325definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    2426
    25 (*CSC: XXXXX *)
    26 axiom rtl_init_locals : list register → register_env beval.
    27 
     27(*CSC: XXXXX, for is_final only *)
    2828axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
    2929
Note: See TracChangeset for help on using the changeset viewer.