Changeset 2952 for src/LIN/LIN.ma


Ignore:
Timestamp:
Mar 26, 2013, 2:01:15 PM (7 years ago)
Author:
tranquil
Message:
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r2946 r2952  
    3434let code ≝
    3535  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
    36    〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4 it) it〉 ;
     36   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
    3737   〈Some ? l3, GOTO ? l3〉 ] in
    3838mk_joint_internal_function LIN (prog_var_names … p)
Note: See TracChangeset for help on using the changeset viewer.