Changeset 1388 for src/RTL

Timestamp:

Oct 17, 2011, 10:54:50 AM (9 years ago)

Author:

sacerdot

Message:

fetch_result implemented for ERTL. This required a different istantiation of
resultT that is not in line with the OCaml's code. Look at CHANGES for details.
RTLToERTL has been ported in an hopefully correct manner.

File:

• src/RTL/RTLToERTL.ma (modified) (1 diff)

src/RTL/RTLToERTL.ma

@@ -354 +354 @@
   let def' ≝
     mk_joint_internal_function globals (ertl_params globals)
-      (joint_if_luniverse … def) (joint_if_runiverse … def) it
+      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
       nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
       graph' ? ? in