Changeset 1388 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
Oct 17, 2011, 10:54:50 AM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r1352 r1388  
    354354  let def' ≝
    355355    mk_joint_internal_function globals (ertl_params globals)
    356       (joint_if_luniverse … def) (joint_if_runiverse … def) it
     356      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
    357357      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    358358      graph' ? ? in
Note: See TracChangeset for help on using the changeset viewer.