|
../
|
|
ASM
|
|
2910
|
8 years
|
sacerdot |
Abstract statuses for ASM and OC completed.
A simple test program can …
|
|
Clight
|
|
2877
|
8 years
|
garnier |
Correction of a bug in my former bug correction.
|
|
Cminor
|
|
2936
|
8 years
|
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
common
|
|
2927
|
8 years
|
tranquil |
stupid bug in bool_of_beval
|
|
ERTL
|
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
ERTLptr
|
|
2949
|
8 years
|
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
joint
|
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
LIN
|
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
LTL
|
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
RTL
|
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
RTLabs
|
|
2948
|
8 years
|
campbell |
Finish up measurable to structured proof, exposing the prefix and …
|
|
utilities
|
|
2949
|
8 years
|
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
root
|
26 bytes
|
703
|
10 years
|
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
Makefile
|
439 bytes
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
TODO
|
606 bytes
|
1457
|
9 years
|
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
BACKEND_BROKEN_FILES
|
713 bytes
|
2754
|
8 years
|
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
semantics.ma
|
2.8 KB
|
2905
|
8 years
|
sacerdot |
Semantics of ASM in place (up to return values and function call …
|
|
CHANGES
|
3.4 KB
|
1388
|
9 years
|
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
compiler.ma
|
5.4 KB
|
2946
|
8 years
|
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
redundant_includes.txt
|
6.8 KB
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
acc-matita-printers.patch
|
7.1 KB
|
1633
|
9 years
|
campbell |
Update Cminor pretty printer and examples.
|
|
correctness.ma
|
7.6 KB
|
2928
|
8 years
|
tranquil |
some sketches about correctness proof
|
