source: src/common @ 2608

Name Size Rev Age Author Last Change
../
Order.ma 117 bytes 1049   10 years mulligan more stuff added
CostLabel.ma 233 bytes 1268   10 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
Smallstep.ma 27.7 KB 1510   10 years sacerdot All files ported to new dependent inversion.
PreIdentifiers.ma 582 bytes 1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
AssocList.ma 767 bytes 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Floats.ma 2.7 KB 1599   10 years sacerdot Start of merging of stuff into the standard library of Matita.
Graphs.ma 1.6 KB 1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
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 * …
AST.ma 29.6 KB 2468   9 years garnier Floats are gone from the front-end. Some trace amount might remain in …
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 …
IO.ma 2.6 KB 2468   9 years garnier Floats are gone from the front-end. Some trace amount might remain in …
Values.ma 29.8 KB 2468   9 years garnier Floats are gone from the front-end. Some trace amount might remain in …
Executions.ma 8.8 KB 2487   9 years campbell Set up "after_n_steps" to enforce an invariant on states.
SmallstepExec.ma 11.7 KB 2487   9 years campbell Set up "after_n_steps" to enforce an invariant on states.
Errors.ma 8.7 KB 2500   9 years garnier Continuing work on simulation in Clight/Cminor?
Animation.ma 4.5 KB 2533   9 years campbell Some fall out from removing floats.
BackEndOps.ma 10.3 KB 2548   9 years tranquil in BackEndOps?, cleaner def of be_op2 new statement of …
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   8 years garnier Some progress on CL to CM.
ExtraMonads.ma 10.6 KB 2590   8 years piccolo added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
Measurable.ma 5.3 KB 2596   8 years campbell Use a simpler stack cost map, and then specialise to each semantics.
FEMeasurable.ma 3.5 KB 2597   8 years campbell Some work in progress on measurable subtrace preservation.
Identifiers.ma 38.2 KB 2599   8 years tranquil * map_opt and map on positive maps are now clean (erase empty …
PositiveMap.ma 32.0 KB 2599   8 years tranquil * map_opt and map on positive maps are now clean (erase empty …
Registers.ma 450 bytes 2603   8 years piccolo Dead code commented out.
BitVectorTrieMap.ma 2.4 KB 2604   8 years piccolo ERTLtoERTLptr in place.
ByteValues.ma 9.3 KB 2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
extraGlobalenvs.ma 8.2 KB 2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
GenMem.ma 7.3 KB 2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
Globalenvs.ma 77.1 KB 2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
Pointers.ma 6.3 KB 2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
Note: See TracBrowser for help on using the repository browser.