source: src/common @ 2695

Name Size Rev Age Author Last Change
../
Order.ma 117 bytes 1049   10 years mulligan more stuff added
Smallstep.ma 27.7 KB 1510   10 years sacerdot All files ported to new dependent inversion.
AssocList.ma 767 bytes 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Integers.ma 77.6 KB 2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
LabelledObjects.ma 10.3 KB 2133   9 years boender - moved does_not_occur_occur_absurd
FrontEndMem.ma 2.0 KB 2429   9 years garnier Restrict semantics of pointer comparison to what CompCert? does - i.e. …
IOMonad.ma 15.1 KB 2453   9 years tranquil come changes in monad notation to * avoid pretty printed monsters * …
Events.ma 10.8 KB 2468   9 years garnier Floats are gone from the front-end. Some trace amount might remain in …
FrontEndVal.ma 2.5 KB 2468   9 years garnier Floats are gone from the front-end. Some trace amount might remain in …
StatusSimulation.ma 38.0 KB 2553   9 years tranquil as_classify changed to a partial function added a status for tailcalls
StructuredTraces.ma 37.8 KB 2553   9 years tranquil as_classify changed to a partial function added a status for tailcalls
FrontEndOps.ma 22.9 KB 2582   9 years garnier Some progress on CL to CM.
ExtraMonads.ma 10.6 KB 2590   9 years piccolo added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
BitVectorTrieMap.ma 2.4 KB 2604   9 years piccolo ERTLtoERTLptr in place.
extraGlobalenvs.ma 8.2 KB 2608   9 years garnier Regions are no more stored in blocks. block_region now tests the id, …
GenMem.ma 7.3 KB 2608   9 years garnier Regions are no more stored in blocks. block_region now tests the id, …
Pointers.ma 6.4 KB 2641   9 years piccolo defined dummy block code equals to 0
Animation.ma 4.5 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
AST.ma 29.5 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
BackEndOps.ma 10.2 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
ByteValues.ma 9.2 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
CostLabel.ma 208 bytes 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Errors.ma 8.7 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Globalenvs.ma 77.1 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Graphs.ma 1.6 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Identifiers.ma 38.2 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
IO.ma 2.5 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Registers.ma 422 bytes 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
Values.ma 29.8 KB 2645   9 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
PreIdentifiers.ma 769 bytes 2646   9 years sacerdot A tag was classified as an error message. Fixed.
ErrorMessages.ma 2.1 KB 2668   9 years campbell Intermediate measurable proof check-in before I change its traces again.
PositiveMap.ma 32.0 KB 2673   9 years tranquil corrected some compilation errors (that might depend on some matita update)
Executions.ma 8.8 KB 2682   9 years campbell Don't apply inv in after_n_steps to last state.
Measurable.ma 16.1 KB 2685   9 years campbell Progress on measurable trace preservation: prefix preserves observable …
SmallstepExec.ma 22.0 KB 2685   9 years campbell Progress on measurable trace preservation: prefix preserves observable …
FEMeasurable.ma 25.6 KB 2690   9 years campbell Most of the measurable subtrace preservation proof done.
Note: See TracBrowser for help on using the repository browser.