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   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   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   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.