source: src/utilities @ 2876

Name Size Rev Age Author Last Change
../
adt 2772   7 years sacerdot Useless code removed.
binary 2310   7 years garnier Moved a lemma from switchRemoval to positive.
bind_new.ma 3.3 KB 1976   8 years tranquil * monads: just changed some defs, which had to be propagated in some …
bindLists.ma 1.3 KB 2155   7 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
BitVectorTrieSet.ma 2.2 KB 753   9 years mulligan Work from today.
Coqlib.ma 31.7 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
deqsets_extra.ma 604 bytes 2716   7 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
extra_bool.ma 205 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extralib.ma 7.9 KB 2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
extranat.ma 5.0 KB 2824   7 years tranquil * moved sum on lists notation to extranat * used sum on lists to …
fixpoints.ma 806 bytes 2700   7 years sacerdot 1. exponential function dropped in favour of standard library 2. …
hide.ma 1.2 KB 2200   7 years tranquil * updated joint semantics: generation of linear and graph semantics * …
listb_extra.ma 381 bytes 2728   7 years sacerdot listb.ma => listb_extra.ma for extraction
lists.ma 10.6 KB 2800   7 years campbell Tidy up Measurable.ma a little, get rid of obsolete comments.
monad.ma 12.1 KB 2529   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
option.ma 2.8 KB 2770   7 years mckinna WARNING: another big commit, touching many files in ASM/*.ma This …
permutations.ma 10.5 KB 1976   8 years tranquil * monads: just changed some defs, which had to be propagated in some …
proper.ma 756 bytes 1908   8 years fguidi notation fixup following last commit of matita we shifted the levels …
RegisterSet.ma 1.7 KB 1193   8 years mulligan work on colouring algorithm halted as it can be axiomatised. now …
setoids.ma 1.4 KB 1635   8 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
state.ma 1.5 KB 2708   7 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
trace.ma 895 bytes 1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
Note: See TracBrowser for help on using the repository browser.