source: src/utilities @ 2919

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