Changeset 2505 for src/RTLabs


Ignore:
Timestamp:
Nov 29, 2012, 3:37:22 PM (7 years ago)
Author:
mckinna
Message:

Cleaned up compiler.ma; some refactoring/additional code needed in Clight/label, and a tweak to translate_cst in RTLabsToRTL to restore its checked status.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2493 r2505  
    161161  λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf).
    162162
    163 include alias "common/Identifiers.ma".
     163(*include alias "common/Identifiers.ma".*)
    164164let rec rtl_args (args : list register) (env : local_env) on args :
    165165  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
Note: See TracChangeset for help on using the changeset viewer.