source: src/common/Identifiers.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1092   9 years campbell Some minor definitions for identifiers and lists.
(edit) @1077   10 years mulligan ack, dependent types are scary
(edit) @1072   10 years campbell Use not equals form of showing entry/exit labels.
(edit) @1070   10 years campbell Show that entry and exit labels are in the RTLabs graph.
(edit) @1068   10 years mulligan rtlabs translation complete subject to axioms
(edit) @1058   10 years campbell Evict CompCert? Maps interface in favour of BitVectorTries?.
(edit) @1057   10 years mulligan changes from today
(edit) @1056   10 years campbell Switch to delayed identifier error scheme.
(edit) @1055   10 years mulligan changes to how identifiers are generated
(edit) @1053   10 years mulligan changes
(edit) @816   10 years campbell Clight to Cminor compilation, modulo switch statements, temporary …
(edit) @797   10 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.