source: src/common @ 1480

Name Size Rev Age Author Last Change
../
Animation.ma 4.6 KB 1231   8 years campbell Change SmallstepExec? so that states can depend on global information. …
AssocList.ma 760 bytes 789   9 years mulligan More work on rtlabs -> rtl pass.
AST.ma 21.6 KB 1465   8 years sacerdot Dead code removed.
CostLabel.ma 233 bytes 1268   8 years sacerdot 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
Errors.ma 11.1 KB 1355   8 years sacerdot monadic fold_lefti added
Events.ma 10.8 KB 961   8 years campbell Use precise bitvector sizes throughout the front end, rather than …
Floats.ma 2.7 KB 961   8 years campbell Use precise bitvector sizes throughout the front end, rather than …
FrontEndOps.ma 17.5 KB 1410   8 years campbell Remove a few old workarounds.
GenMem.ma 6.6 KB 1395   8 years sacerdot 1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
Globalenvs.ma 52.0 KB 1395   8 years sacerdot 1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
Graphs.ma 1.0 KB 1253   8 years mulligan uses.ma finished
Identifiers.ma 8.4 KB 1316   8 years campbell Merge in id-lookup-branch to trunk.
Integers.ma 77.7 KB 1480   8 years sacerdot Proof changed (to use new automation). BUG FOUND: automation fails if …
IO.ma 2.6 KB 961   8 years campbell Use precise bitvector sizes throughout the front end, rather than …
IOMonad.ma 8.3 KB 797   9 years campbell Add error messages wherever the error monad is used. Sticks to …
Mem.ma 114.1 KB 891   9 years campbell Revise proofs affected by recent matita change.
Order.ma 117 bytes 1049   8 years mulligan more stuff added
Pointers.ma 4.1 KB 1215   8 years sacerdot 1) Added shifting directly on pointers 2) More temporary axioms closed.
PreIdentifiers.ma 572 bytes 797   9 years campbell Add error messages wherever the error monad is used. Sticks to …
Registers.ma 436 bytes 1129   8 years mulligan removed conversions between Register and register
Smallstep.ma 27.7 KB 891   9 years campbell Revise proofs affected by recent matita change.
SmallstepExec.ma 4.8 KB 1233   8 years sacerdot 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
Values.ma 30.8 KB 1369   8 years campbell Put type information into front-end unary ops. Slight change to …
Note: See TracBrowser for help on using the repository browser.