|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
@749
|
10 years |
campbell |
Make definition more explicit to avoid jmeq.
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
@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.
|
|
|
@722
|
10 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
@719
|
10 years |
mulligan |
Added missing assembly file ported to matita.
|
|
|
@715
|
10 years |
mulligan |
Restored rev from Util as it appears that list reversal is not a part …
|
|
|
@714
|
10 years |
mulligan |
Work on translation from LTL to LIN.
|
|
|
@712
|
10 years |
mulligan |
Changes to get things to typecheck.
|
|
|
@706
|
10 years |
sacerdot |
Fixed (reference to basics/pairs was dandling).
|
|
|
@705
|
10 years |
sacerdot |
Ported to new library (notation).
|
|
|
@704
|
10 years |
sacerdot |
Minor speedup in one theorem (less automation).
|
|
|
@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.
|
|
|
@696
|
10 years |
mulligan |
Added missing I8051 file and completed most of LIN formalisation.
|
|
|
@690
|
10 years |
mulligan |
Moved new matita files into correct place.
|
|
|
@689
|
10 years |
mulligan |
Got rid of old Matita development files.
|
|
|
@688
|
10 years |
mulligan |
Fixed local conflicts. Restructured svn repository.
|
|
copied from Deliverables/D4.1/Matita:
|
|
|
@664
|
10 years |
mulligan |
Changed output of Intel HEX files so we no longer have those …
|