Changeset 1352 for src/ERTL


Ignore:
Timestamp:
Oct 11, 2011, 12:45:16 PM (9 years ago)
Author:
sacerdot
Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1282 r1352  
    199199    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    200200    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    201       〈add_graph globals original_label (sequential (ltl_params globals) globals (INT globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
     201      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    202202
    203203definition translate_statement:
Note: See TracChangeset for help on using the changeset viewer.