Changeset 1254 for src/joint

Timestamp:

Sep 22, 2011, 4:16:06 PM (8 years ago)

Author:

sacerdot

Message:

More progress towards porting of RTLtoERTL to joint syntax.

File:

• src/joint/Joint.ma (modified) (1 diff)

src/joint/Joint.ma

@@ -99 +99 @@
     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
 
+definition set_runiverse ≝
+  λglobals,pars.
+  λp : joint_internal_function globals pars.
+  λruniverse: universe RegisterTag.
+   mk_joint_internal_function globals pars
+    (joint_if_luniverse … p) runiverse (joint_if_result … p)
+    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
+    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
+
 (* Specialized for graph_params *)
 definition add_graph ≝