Ignore:
Timestamp:
Sep 26, 2011, 2:52:22 PM (8 years ago)
Author:
sacerdot
Message:

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/CostLabel.ma

    r757 r1268  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    9 
    10 (* dpm: fix identifier/costlabel mismatch *)
    11 axiom Identifier_of_costlabel: costlabel → Identifier.
Note: See TracChangeset for help on using the changeset viewer.