|
|
|
@2782
|
8 years |
sacerdot |
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end 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
|
9 years |
sacerdot |
Proof improved (for case 3) + new proof (for case 11)
|
|
|
|
@2124
|
9 years |
sacerdot |
Much more shuffling around to proper places
|
|
|
|
@2122
|
9 years |
sacerdot |
More stuff moved around in proper places
|
|
|
|
@2121
|
9 years |
sacerdot |
More functions moved to the places they belong to
|
|
|
|
@2006
|
9 years |
boender |
- added alias for bitvector zero
- changed extralib bounded …
|
|
|
|
@1928
|
9 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
|
@1890
|
9 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
|
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 …
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@868
|
10 years |
mulligan |
more changes
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@726
|
10 years |
campbell |
Change identifiers to Words in Clight and RTLabs semantics.
|
|
|
|
@724
|
10 years |
campbell |
More tractable version of bitvector_of_nat / nat_of_bitvector.
|
|
|
|
@700
|
10 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@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/BitVector.ma:
|
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
