Changeset 1450

Timestamp:

Oct 21, 2011, 10:37:22 PM (8 years ago)

Author:

sacerdot

Message:

Disambiguation problem avoided.

File:

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

src/RTL/RTLToERTL.ma

@@ -346 +346 @@
   λglobals.λdef:rtlntc_internal_function globals.
   let nb_params ≝ |joint_if_params ?? def| in
-  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
+  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
   let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
   let entry' ≝ joint_if_entry … def in