|
../
|
|
ASM
|
|
3039
|
8 years
|
tranquil |
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
|
|
Clight
|
|
3036
|
8 years
|
garnier |
Fixing some problems, progress, etc
|
|
Cminor
|
|
3007
|
8 years
|
campbell |
Sketch out how Cminor to RTLabs correctness would fit into the …
|
|
common
|
|
3032
|
8 years
|
campbell |
Remind myself why ms_rel_normal is reasonable.
|
|
ERTL
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
ERTLptr
|
|
3018
|
8 years
|
sacerdot |
1) some files repaired
2) all stuff related to the aborted pass …
|
|
joint
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
LIN
|
|
3039
|
8 years
|
tranquil |
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
|
|
LTL
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
RTL
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
RTLabs
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
utilities
|
|
2949
|
8 years
|
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
acc-matita-printers.patch
|
7.1 KB
|
1633
|
9 years
|
campbell |
Update Cminor pretty printer and examples.
|
|
BACKEND_BROKEN_FILES
|
713 bytes
|
2754
|
8 years
|
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
CHANGES
|
3.4 KB
|
1388
|
9 years
|
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
compiler.ma
|
5.4 KB
|
3022
|
8 years
|
campbell |
Make a couple of tests monadic for easier inversion.
|
|
correctness.ma
|
6.8 KB
|
3030
|
8 years
|
campbell |
Break up front-end for correctness proof.
Use let rec to prevent …
|
|
Makefile
|
439 bytes
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
redundant_includes.txt
|
6.8 KB
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
root
|
26 bytes
|
703
|
10 years
|
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
semantics.ma
|
2.6 KB
|
3035
|
8 years
|
mckinna |
Tweak: tidied up ?/\ldots
Conceptual: better monadic threading of …
|
|
TODO
|
606 bytes
|
1457
|
9 years
|
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
