

@1602

9 years 
mulligan 
giving up on fetch proofs for time being



@1600

9 years 
sacerdot 
utilities and ASM ported to the new standard library



@1599

9 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1598

9 years 
mulligan 
changes over the last couple of days



@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 rtlertl 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/newmatitadevelopment/Util.ma:



@688

10 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
