|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1323
|
9 years |
campbell |
Reduce number of notations for destructive let on pairs to one.
|
|
|
|
@1279
|
9 years |
sacerdot |
Bug fixed in definition of ltb.
|
|
|
|
@1193
|
9 years |
mulligan |
work on colouring algorithm halted as it can be axiomatised. now …
|
|
|
|
@1161
|
9 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
|
@1159
|
9 years |
boender |
- added 'nth' theorems
- moved up \bot a bit
|
|
|
|
@1094
|
9 years |
mulligan |
some changes from today to do with liveness analyses
|
|
|
|
@1075
|
10 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@1064
|
10 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
|
@1063
|
10 years |
mulligan |
changes from today
|
|
|
|
@1062
|
10 years |
mulligan |
separated jmeq and coercions from foldstuff.ma in order to fix the …
|
|
|
|
@1061
|
10 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
|
@1060
|
10 years |
mulligan |
work from this morning and yesterday
|
|
|
|
@1059
|
10 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
|
@1057
|
10 years |
mulligan |
changes from today
|
|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
|
@993
|
10 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
|
@990
|
10 years |
sacerdot |
Do no longer use the daemon automatically :-)
|
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
|
@907
|
10 years |
boender |
- added quadruples to Util
- start of implementation of new jump …
|
|
|
|
@900
|
10 years |
sacerdot |
New implementation of flatten was bugged: fixed.
|
|
|
|
@899
|
10 years |
mulligan |
changed defn. of flatten
|
|
|
|
@858
|
10 years |
sacerdot |
If then else notation improved.
|
|
|
|
@857
|
10 years |
sacerdot |
Notations.
|
|
|
|
@856
|
10 years |
sacerdot |
1. if_then_else is now a notation for match with (to allow Russell to …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@777
|
10 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
|
@715
|
10 years |
mulligan |
Restored rev from Util as it appears that list reversal is not a part …
|
|
|
|
@712
|
10 years |
mulligan |
Changes to get things to typecheck.
|
|
|
|
@704
|
10 years |
sacerdot |
Minor speedup in one theorem (less automation).
|
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
|
@697
|
10 years |
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
|
|
@690
|
10 years |
mulligan |
Moved new matita files into correct place.
|
|
copied from src/ASM/new-matita-development/Util.ma:
|
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
