source: src/common/Identifiers.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1949   8 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
(edit) @1928   8 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
(edit) @1908   9 years fguidi notation fixup following last commit of matita we shifted the levels …
(edit) @1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1635   9 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1631   9 years campbell Use fact that type environments in Cminor have distinct variables to …
(edit) @1627   9 years campbell Add some notions of freshness, and start using them for temporary …
(edit) @1601   9 years sacerdot Files ported to new version of the standard library.
(edit) @1562   9 years mulligan new version of assembly, fixed conflict in positivemap.ma, changed …
(edit) @1535   9 years campbell Make RTLabs semantics use knowledge that the next instruction always …
(edit) @1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
(edit) @1515   9 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1316   9 years campbell Merge in id-lookup-branch to trunk.
(edit) @1092   9 years campbell Some minor definitions for identifiers and lists.
(edit) @1077   9 years mulligan ack, dependent types are scary
(edit) @1072   9 years campbell Use not equals form of showing entry/exit labels.
(edit) @1070   9 years campbell Show that entry and exit labels are in the RTLabs graph.
(edit) @1068   9 years mulligan rtlabs translation complete subject to axioms
(edit) @1058   9 years campbell Evict CompCert? Maps interface in favour of BitVectorTries?.
(edit) @1057   9 years mulligan changes from today
(edit) @1056   9 years campbell Switch to delayed identifier error scheme.
(edit) @1055   9 years mulligan changes to how identifiers are generated
(edit) @1053   9 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   10 years mulligan More work on rtl-ertl pass from today, plus resolved conflict.
(edit) @779   10 years campbell Add merging of tries and identifier sets (based on Dominic's earlier …
(edit) @761   10 years campbell Enforce the use of declared identifiers/registers in Cminor/RTLabs.
(edit) @757   10 years mulligan Lots more fixing to get both front and backends using same conventions …
(edit) @753   10 years mulligan Work from today.
(edit) @738   10 years campbell Use lower case names for identifiers for consistency with CompCert?
(edit) @737   10 years campbell Use more abstract identifiers in Clight / RTLabs.
(add) @736   10 years campbell Extra type safety for identifiers.
Note: See TracRevisionLog for help on using the revision log.