Changeset 1388 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Oct 17, 2011, 10:54:50 AM (10 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/ERTL/ERTL.ma

    r1280 r1388  
    1414  register nat unit ertl_statement_extension.
    1515definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
    16 definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ (list register) nat.
    1717definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
    1818definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
Note: See TracChangeset for help on using the changeset viewer.