Changeset 2674 for src/ERTL/ERTL_semantics.ma

Timestamp:

Feb 18, 2013, 5:48:19 PM (7 years ago)

Author:

tranquil

Message:

• another change in block definition
• RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken

File:

• src/ERTL/ERTL_semantics.ma (modified) (1 diff)

src/ERTL/ERTL_semantics.ma

@@ -142 +142 @@
   (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
-         
+
 definition ERTL_semantics ≝
-  make_sem_graph_params ERTL ERTL_sem_uns.
+  mk_sem_graph_params ERTL ERTL_sem_uns.