Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN.ma

    r2286 r2490  
    44 | from_acc: Register → unit → registers_move
    55 | to_acc: unit → Register → registers_move
    6  | int_to_reg : Register → beval → registers_move
    7  | int_to_acc : unit → beval → registers_move.
     6 | int_to_reg : Register → Byte → registers_move
     7 | int_to_acc : unit → Byte → registers_move.
    88(* the last is redudant, but kept for notation's sake *)
    99
     
    2626    (* call_dest ≝ *) unit
    2727    (* ext_seq ≝ *) ltl_lin_seq
    28     (* ext_call ≝ *) void
    29     (* ext_tailcall ≝ *) void
     28    (* has_tailcalls ≝ *) false
    3029    (* paramsT ≝ *) unit
    3130    (* localsT ≝ *) void.
Note: See TracChangeset for help on using the changeset viewer.