Changeset 1386 for src/RTL

Timestamp:

Oct 17, 2011, 1:58:47 AM (9 years ago)

Author:

sacerdot

Message:

Structure of semantic parameters simplified.

File:

• src/RTL/semantics.ma (modified) (2 diffs)

src/RTL/semantics.ma

@@ -88 +88 @@
 qed.
 
-definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
- mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
-  rtl_init_locals rtl_save_frame.
-
 (*CSC: XXXX, for external functions only*)
 axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
@@ -117 +113 @@
 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
  λglobals.
-  mk_more_sem_params2 … rtl_more_sem_params1
+  mk_more_sem_params2 … rtl_more_sem_params
    (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
-   (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
+   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
+   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
 
 definition rtl_fullexec ≝