Changeset 1278 for src/RTL/RTL.ma


Ignore:
Timestamp:
Sep 27, 2011, 9:57:12 AM (9 years ago)
Author:
sacerdot
Message:

oppargs requires two more arguments. RTLtoERTL to be fixed since it was
bugged anyway

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1275 r1278  
    1414  (mk_params__ register register register register
    1515    (register × register) register (list register) (list register)
    16       rtl_statement_extension unit (list register) (list register)) label.
     16      rtl_statement_extension (list register) (list register) (list register)) label.
    1717
    1818definition rtl_statement ≝ joint_statement rtl_params_.
     
    3333inductive rtlntc_statement_extension: Type[0] ≝
    3434  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
    35   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension
    36   | rtlntc_st_ext_tailcall_id: ident → list register → rtlntc_statement_extension
    37   | rtlntc_st_ext_tailcall_ptr: register → register → list register → rtlntc_statement_extension.
     35  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    3836
    3937definition rtlntc_params_: params_ ≝
     
    4139  (mk_params__ register register register register
    4240    (register × register) register (list register) (list register)
    43       rtlntc_statement_extension unit (list register) (list register)) label.
     41      rtlntc_statement_extension (list register) (list register) (list register)) label.
    4442
    4543definition rtlntc_statement ≝ joint_statement rtlntc_params_.
Note: See TracChangeset for help on using the changeset viewer.