

@2700

8 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2673

8 years 
tranquil 
corrected some compilation errors (that might depend on some matita update)



@2314

8 years 
campbell 
Move generic definitions from recent commit to appropriate places.



@2307

8 years 
campbell 
Half the proofs for sound cost labelling check.



@2286

8 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2211

8 years 
boender 
 finished proof of sigma specification
 added some stuff to Util, as …



@2149

8 years 
sacerdot 
Code shuffling to proper places.



@2125

8 years 
boender 
 some more displacement from Policy to Util



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2123

8 years 
boender 
 moved is_well_labeled_p to Status and instruction_is_label to ASM
…



@2111

8 years 
sacerdot 
Cleanup: lemmas/theorems/axioms moved to the right places.



@2055

8 years 
sacerdot 
Warning: this commit adds an hypothesis that breaks all of assembly stuff.



@2037

8 years 
sacerdot 
flatten is now part of stdlib



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2005

8 years 
boender 
 minor changes to make things compile with a clean checkout



@1964

8 years 
tranquil 
introduced as_label_of_cost and adapted accordingly. Equality of cost …



@1937

8 years 
boender 
 filled in some of the gaps in the proof of Policy
 reverted …



@1934

8 years 
boender 
 various & sundry moves of lemmas to better places
 integrated …



@1928

8 years 
mulligan 
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …



@1908

8 years 
fguidi 
notation fixup following last commit of matita
we shifted the levels …



@1882

8 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1811

9 years 
boender 
 corrected definition of geb



@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

9 years 
mulligan 
nearly completed rtl > ertl pass removing all option types with dep. types



@1071

9 years 
mulligan 
changes the specific form that the added proofs take to use None, not …



@1064

9 years 
mulligan 
changes from today, nearly complete rtlabs translation pass



@1063

9 years 
mulligan 
changes from today



@1062

9 years 
mulligan 
separated jmeq and coercions from foldstuff.ma in order to fix the …



@1061

9 years 
mulligan 
more work, bug found, ridiculous map3 function with dep. types added



@1060

9 years 
mulligan 
work from this morning and yesterday



@1059

9 years 
mulligan 
work from today, bit of a mess at the moment



@1057

9 years 
mulligan 
changes from today



@998

9 years 
sacerdot 
Half repaired, half broken. Most functions no longer return option …



@993

9 years 
sacerdot 
More Russell everywhere; getting closer to the goal.



@990

9 years 
sacerdot 
Do no longer use the daemon automatically :)



@985

9 years 
sacerdot 
1) Major refactoring: proofs moved where they should be.
2) New …



@907

9 years 
boender 
 added quadruples to Util
 start of implementation of new jump …



@900

9 years 
sacerdot 
New implementation of flatten was bugged: fixed.



@899

9 years 
mulligan 
changed defn. of flatten



@858

9 years 
sacerdot 
If then else notation improved.



@857

9 years 
sacerdot 
Notations.



@856

9 years 
sacerdot 
1. if_then_else is now a notation for match with (to allow Russell to …



@782

9 years 
mulligan 
More work on rtlertl pass from today, plus resolved conflict.



@777

9 years 
mulligan 
Lots of work on RTL to ERTL pass from today.



@764

9 years 
campbell 
Start Cminor to RTLabs phase.
Includes some syntax for matching …



@746

9 years 
mulligan 
Changes to bitvectortrieset: equality on sets. Added new file for …



@715

9 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.
