Changeset 1242 for src/ERTL/ERTL.ma

Timestamp:

Sep 21, 2011, 5:35:54 PM (9 years ago)

Author:

sacerdot

Message:

Some clean-up.

File:

• src/ERTL/ERTL.ma (modified) (2 diffs)

src/ERTL/ERTL.ma

@@ -1 +1 @@
 include "joint/Joint.ma".
-include "common/Graphs.ma".
-
-definition registers ≝ list register.
 
 inductive move_registers: Type[0] ≝
@@ -13 +10 @@
   | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
 
-definition ertl_params_: params_ ≝
-  mk_params_ register register register register
+definition ertl_params: params ≝
+ mk_params
+  (mk_params_ register register register register
     (move_registers × move_registers) register
-      ertl_statement_extension unit (list register) nat.
-
-definition ertl_params: params ≝
-  mk_params ertl_params_ label.
+      ertl_statement_extension unit (list register) nat) label.
 
 definition ertl_statement ≝ joint_statement ertl_params.
 
-(*
-definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
- λglobals.
-  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
-*)
-
-definition ertl_internal_function ≝
-  joint_internal_function ertl_params.
+definition ertl_internal_function ≝ joint_internal_function ertl_params.
 
 definition ertl_program ≝ joint_program ertl_params.