|
../
|
|
utilities
|
|
3050
|
8 years
|
piccolo |
1) Added general commutation theorem for monads.
2) Added some …
|
|
RTLabs
|
|
3050
|
8 years
|
piccolo |
1) Added general commutation theorem for monads.
2) Added some …
|
|
RTL
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
LTL
|
|
3037
|
8 years
|
tranquil |
* ADDRESS joint instruction now has also an offset
* corrected call to …
|
|
LIN
|
|
3066
|
8 years
|
tranquil |
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …
|
|
joint
|
|
3050
|
8 years
|
piccolo |
1) Added general commutation theorem for monads.
2) Added some …
|
|
ERTLptr
|
|
3018
|
8 years
|
sacerdot |
1) some files repaired
2) all stuff related to the aborted pass …
|
|
ERTL
|
|
3072
|
8 years
|
tranquil |
corrected a bug (translate_store was wrong)
|
|
common
|
|
3063
|
8 years
|
campbell |
Remove measure function from FEMeasurable because we're not using it …
|
|
Cminor
|
|
3063
|
8 years
|
campbell |
Remove measure function from FEMeasurable because we're not using it …
|
|
Clight
|
|
3063
|
8 years
|
campbell |
Remove measure function from FEMeasurable because we're not using it …
|
|
ASM
|
|
3075
|
8 years
|
mckinna |
Apologies for late folding in of old changes which were left over from …
|
|
TODO
|
606 bytes
|
1457
|
9 years
|
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
semantics.ma
|
2.6 KB
|
3035
|
8 years
|
mckinna |
Tweak: tidied up ?/\ldots
Conceptual: better monadic threading of …
|
|
root
|
26 bytes
|
703
|
10 years
|
sacerdot |
lib is now the default standard library (after commit 11216 in …
|
|
redundant_includes.txt
|
6.8 KB
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
Makefile
|
439 bytes
|
2919
|
8 years
|
fguidi |
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
|
|
correctness.ma
|
8.3 KB
|
3074
|
8 years
|
campbell |
Put some kind of high level proof in for front-end.
|
|
compiler.ma
|
5.4 KB
|
3022
|
8 years
|
campbell |
Make a couple of tests monadic for easier inversion.
|
|
CHANGES
|
3.4 KB
|
1388
|
10 years
|
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
BACKEND_BROKEN_FILES
|
713 bytes
|
2754
|
8 years
|
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
acc-matita-printers.patch
|
7.1 KB
|
1633
|
9 years
|
campbell |
Update Cminor pretty printer and examples.
|
