

@2645

8 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2601

8 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2126

8 years 
sacerdot 
Proof improved (for case 3) + new proof (for case 11)



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2122

8 years 
sacerdot 
More stuff moved around in proper places



@2121

8 years 
sacerdot 
More functions moved to the places they belong to



@2006

8 years 
boender 
 added alias for bitvector zero
 changed extralib bounded …



@1928

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



@1890

8 years 
boender 
 added comment about bitvector translation



@1635

9 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1599

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



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@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 …



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@868

9 years 
mulligan 
more changes



@744

9 years 
campbell 
Evict Coqstyle integers from common/Integers.ma.
Make more bitvector …



@726

9 years 
campbell 
Change identifiers to Words in Clight and RTLabs semantics.



@724

9 years 
campbell 
More tractable version of bitvector_of_nat / nat_of_bitvector.



@700

9 years 
campbell 
Get Clight semantics going again (except for problems CexecEquiv? that …



@698

9 years 
mulligan 
Commit with changes to files to get our files to typecheck.



@697

9 years 
campbell 
Merge Clight branch of vectors and friends.
Start making stuff build.



@690

9 years 
mulligan 
Moved new matita files into correct place.


copied from src/ASM/newmatitadevelopment/BitVector.ma:



@688

9 years 
mulligan 
Fixed local conflicts. Restructured svn repository.
