source: src/common/Identifiers.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1627   8 years campbell Add some notions of freshness, and start using them for temporary …
(edit) @1601   8 years sacerdot Files ported to new version of the standard library.
(edit) @1562   8 years mulligan new version of assembly, fixed conflict in positivemap.ma, changed …
(edit) @1535   8 years campbell Make RTLabs semantics use knowledge that the next instruction always …
(edit) @1516   8 years sacerdot Ported to syntax of Matita 0.99.1.
(edit) @1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1316   8 years campbell Merge in id-lookup-branch to trunk.
(edit) @1092   8 years campbell Some minor definitions for identifiers and lists.
(edit) @1077   8 years mulligan ack, dependent types are scary
(edit) @1072   8 years campbell Use not equals form of showing entry/exit labels.
(edit) @1070   8 years campbell Show that entry and exit labels are in the RTLabs graph.
(edit) @1068   8 years mulligan rtlabs translation complete subject to axioms
(edit) @1058   8 years campbell Evict CompCert? Maps interface in favour of BitVectorTries?.
(edit) @1057   8 years mulligan changes from today
(edit) @1056   8 years campbell Switch to delayed identifier error scheme.
(edit) @1055   8 years mulligan changes to how identifiers are generated
(edit) @1053   8 years mulligan changes
(edit) @816   9 years campbell Clight to Cminor compilation, modulo switch statements, temporary …
(edit) @797   9 years campbell Add error messages wherever the error monad is used. Sticks to …
(edit) @782   9 years mulligan More work on rtl-ertl pass from today, plus resolved conflict.
(edit) @779   9 years campbell Add merging of tries and identifier sets (based on Dominic's earlier …
(edit) @761   9 years campbell Enforce the use of declared identifiers/registers in Cminor/RTLabs.
(edit) @757   9 years mulligan Lots more fixing to get both front and backends using same conventions …
(edit) @753   9 years mulligan Work from today.
(edit) @738   9 years campbell Use lower case names for identifiers for consistency with CompCert?
(edit) @737   9 years campbell Use more abstract identifiers in Clight / RTLabs.
(add) @736   9 years campbell Extra type safety for identifiers.
Note: See TracRevisionLog for help on using the revision log.