Changeset 1175 for src/ERTL/ERTL.ma
 Timestamp:
 Sep 2, 2011, 5:58:01 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r1171 r1175 37 37 }. 38 38 39 definition set_luniverse ≝ 40 λglobals : list ident. 41 λint_fun : ertl_internal_function globals. 42 λluniverse: universe LabelTag. 43 let runiverse ≝ ertl_if_runiverse globals int_fun in 44 let params ≝ ertl_if_params globals int_fun in 45 let locals ≝ ertl_if_locals globals int_fun in 46 let stacksize ≝ ertl_if_stacksize globals int_fun in 47 let graph ≝ ertl_if_graph globals int_fun in 48 let entry ≝ ertl_if_entry globals int_fun in 49 let exit ≝ ertl_if_exit globals int_fun in 50 mk_ertl_internal_function globals 51 luniverse runiverse params locals 52 stacksize graph entry exit. 53 39 54 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 40 55
Note: See TracChangeset
for help on using the changeset viewer.