|
|
@2645
|
7 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2500
|
7 years |
garnier |
Continuing work on simulation in Clight/Cminor?
|
|
|
@2496
|
7 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
@2453
|
7 years |
tranquil |
come changes in monad notation to
* avoid pretty printed monsters
* …
|
|
|
@2439
|
7 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
@1954
|
8 years |
campbell |
Initial state is in the labelling simulation
(modulo global envs results).
|
|
|
@1949
|
8 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1647
|
8 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
@1640
|
8 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
@1626
|
8 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@1609
|
8 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
@1608
|
8 years |
sacerdot |
Porting to new library still in progress.
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
@1599
|
8 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
@1598
|
8 years |
mulligan |
changes over the last couple of days
|
|
|
@1355
|
8 years |
sacerdot |
monadic fold_lefti added
|
|
|
@1351
|
8 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
@1316
|
8 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
@1214
|
8 years |
sacerdot |
res_to_opt function added to common/Errors and used in joint/semantics …
|
|
|
@1125
|
8 years |
sacerdot |
Monadic mfold_left2 added.
|
|
|
@797
|
9 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
@764
|
9 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@695
|
9 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
copied from src/Clight/Errors.ma:
|
|
|
@694
|
9 years |
campbell |
Start moving Clight into common directory.
|