source: extracted @ 3006

Name Size Rev Age Author Last Change
../
untrusted 3002   7 years tranquil fixed previous commit
abstractStatus.ml 4.2 KB 2905   7 years sacerdot Semantics of ASM in place (up to return values and function call …
abstractStatus.mli 1.5 KB 2905   7 years sacerdot Semantics of ASM in place (up to return values and function call …
arithmetic.ml 27.1 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
arithmetic.mli 8.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
aSM.ml 229.8 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
aSM.mli 64.3 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
aSMCosts.ml 30.1 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
aSMCosts.mli 2.0 KB 2910   7 years sacerdot Abstract statuses for ASM and OC completed. A simple test program can …
aSMCostsSplit.ml 3.3 KB 2997   7 years sacerdot New extraction.
aSMCostsSplit.mli 1.3 KB 2997   7 years sacerdot New extraction.
assembly.ml 179.9 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
assembly.mli 3.9 KB 2905   7 years sacerdot Semantics of ASM in place (up to return values and function call …
assocList.ml 979 bytes 2842   7 years sacerdot The compiler can now show all back-end traces too (assembly and object …
assocList.mli 534 bytes 2842   7 years sacerdot The compiler can now show all back-end traces too (assembly and object …
aST.ml 55.2 KB 2997   7 years sacerdot New extraction.
aST.mli 19.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
backEndOps.ml 45.8 KB 3001   7 years sacerdot New extraction.
backEndOps.mli 8.6 KB 2933   7 years sacerdot New extraction, several bug fixed. RTL_semantics fixed by hand, will …
bEMem.ml 1.0 KB 2829   7 years sacerdot Semantics files committed.
bEMem.mli 801 bytes 2829   7 years sacerdot Semantics files committed.
bigops.ml 11.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bigops.mli 5.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bind_new.ml 4.8 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
bind_new.mli 2.2 KB 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
bindLists.ml 1.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bindLists.mli 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bitVector.ml 2.1 KB 2780   7 years sacerdot Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
bitVector.mli 1.1 KB 2780   7 years sacerdot Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …
bitVectorTrie.ml 11.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
bitVectorTrie.mli 3.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bitVectorTrieSet.ml 3.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bitVectorTrieSet.mli 924 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bitVectorZ.ml 2.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
bitVectorZ.mli 743 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
blocks.ml 2.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
blocks.mli 1.7 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
bool.ml 2.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
bool.mli 924 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
build 279 bytes 2789   7 years campbell Some changes to the driver to aid debugging.
byteValues.ml 40.8 KB 3001   7 years sacerdot New extraction.
byteValues.mli 13.8 KB 2933   7 years sacerdot New extraction, several bug fixed. RTL_semantics fixed by hand, will …
casts.ml 892 bytes 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
casts.mli 746 bytes 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
cexec.ml 48.0 KB 3001   7 years sacerdot New extraction.
cexec.mli 3.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
cexecInd.ml 548 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
cexecInd.mli 548 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
cexecSound.ml 875 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
cexecSound.mli 875 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
classifyOp.ml 40.1 KB 3001   7 years sacerdot New extraction.
classifyOp.mli 18.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
clight_abstract.ml 2.8 KB 2803   7 years sacerdot More code extracted, used to debug the compiler.
clight_abstract.mli 1.4 KB 2803   7 years sacerdot More code extracted, used to debug the compiler.
clight_classified_system.ml 1.8 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
clight_classified_system.mli 1.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
cminor_abstract.ml 3.3 KB 2810   7 years sacerdot Cminor semantics exported.
cminor_abstract.mli 1.8 KB 2810   7 years sacerdot Cminor semantics exported.
cminor_classified_system.ml 1.8 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
cminor_classified_system.mli 1.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
cminor_semantics.ml 36.3 KB 3001   7 years sacerdot New extraction.
cminor_semantics.mli 11.1 KB 2810   7 years sacerdot Cminor semantics exported.
cminor_syntax.ml 41.1 KB 3001   7 years sacerdot New extraction.
cminor_syntax.mli 19.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
compiler.ml 24.2 KB 3001   7 years sacerdot New extraction.
compiler.mli 8.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
coqlib.ml 363 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
coqlib.mli 238 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
core_notation.ml 15 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
core_notation.mli 15 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
costCheck.ml 5.1 KB 3001   7 years sacerdot New extraction.
costCheck.mli 1.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costInj.ml 1.9 KB 3001   7 years sacerdot New extraction.
costInj.mli 1.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
costLabel.ml 711 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costLabel.mli 547 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costMisc.ml 816 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costMisc.mli 816 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costSpec.ml 4.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
costSpec.mli 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
csem.ml 50.6 KB 3001   7 years sacerdot New extraction.
csem.mli 13.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
csyntax.ml 56.6 KB 3001   7 years sacerdot New extraction.
csyntax.mli 22.3 KB 3001   7 years sacerdot New extraction.
deqsets.ml 4.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
deqsets.mli 1.8 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
deqsets_extra.ml 454 bytes 2730   7 years sacerdot Exported again.
deqsets_extra.mli 314 bytes 2730   7 years sacerdot Exported again.
div_and_mod.ml 3.4 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
div_and_mod.mli 1.5 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
division.ml 7.2 KB 2827   7 years sacerdot Everything extracted again.
division.mli 1.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
errorMessages.ml 1.3 KB 2997   7 years sacerdot New extraction.
errorMessages.mli 1.3 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
errors.ml 9.5 KB 2997   7 years sacerdot New extraction.
errors.mli 4.5 KB 2743   7 years sacerdot Latest version of the compiler, extracted with the latest version of …
eRTL.ml 25.1 KB 3001   7 years sacerdot New extraction.
eRTL.mli 10.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTL_printer.ml 1.3 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTL_printer.mli 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTL_semantics.ml 11.3 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTL_semantics.mli 3.2 KB 2829   7 years sacerdot Semantics files committed.
eRTLptr.ml 11.9 KB 3001   7 years sacerdot New extraction.
eRTLptr.mli 4.7 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTLptr_printer.ml 1.3 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTLptr_printer.mli 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTLptr_semantics.ml 6.0 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
eRTLptr_semantics.mli 1.6 KB 2829   7 years sacerdot Semantics files committed.
eRTLptrToLTL.ml 38.0 KB 3001   7 years sacerdot New extraction.
eRTLptrToLTL.mli 8.7 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTLToERTLptr.ml 4.6 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
eRTLToERTLptr.mli 1.6 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
events.ml 11.1 KB 2997   7 years sacerdot New extraction.
events.mli 4.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
executions.ml 658 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
executions.mli 658 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
exp.ml 268 bytes 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
exp.mli 177 bytes 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
extra_bool.ml 463 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extra_bool.mli 271 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
extraGlobalenvs.ml 697 bytes 2829   7 years sacerdot Semantics files committed.
extraGlobalenvs.mli 697 bytes 2829   7 years sacerdot Semantics files committed.
extralib.ml 1.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
extralib.mli 635 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
extraMonads.ml 7.0 KB 2829   7 years sacerdot Semantics files committed.
extraMonads.mli 3.6 KB 2829   7 years sacerdot Semantics files committed.
extranat.ml 6.1 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
extranat.mli 2.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
fetch.ml 82.1 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
fetch.mli 1.6 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
fixpoints.ml 10.1 KB 3001   7 years sacerdot New extraction.
fixpoints.mli 5.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
foldStuff.ml 1.5 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
foldStuff.mli 741 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
fresh.ml 2.1 KB 3001   7 years sacerdot New extraction.
fresh.mli 1.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
frontend_misc.ml 6.1 KB 2827   7 years sacerdot Everything extracted again.
frontend_misc.mli 2.2 KB 2827   7 years sacerdot Everything extracted again.
frontEndMem.ml 3.0 KB 3001   7 years sacerdot New extraction.
frontEndMem.mli 1.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
frontEndOps.ml 56.8 KB 3001   7 years sacerdot New extraction.
frontEndOps.mli 23.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
frontEndVal.ml 4.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
frontEndVal.mli 1.2 KB 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
genMem.ml 9.7 KB 3001   7 years sacerdot New extraction.
genMem.mli 4.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
globalenvs.ml 26.2 KB 3001   7 years sacerdot New extraction.
globalenvs.mli 11.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
graphs.ml 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
graphs.mli 833 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
hide.ml 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hide.mli 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hints_declaration.ml 162 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
hints_declaration.mli 162 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
i8051.ml 32.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
i8051.mli 6.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
i8051bis.ml 551 bytes 2829   7 years sacerdot Semantics files committed.
i8051bis.mli 211 bytes 2829   7 years sacerdot Semantics files committed.
identifiers.ml 17.7 KB 2997   7 years sacerdot New extraction.
identifiers.mli 8.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
initialisation.ml 5.5 KB 2797   7 years sacerdot Extracted again after James's cleanup and the implementation of the …
initialisation.mli 1.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
integers.ml 9.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
integers.mli 3.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
interference.ml 8.6 KB 3001   7 years sacerdot New extraction.
interference.mli 4.4 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
interpret2.ml 14.9 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
interpret2.mli 2.6 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
interpret.ml 245.5 KB 2909   7 years sacerdot New extraction.
interpret.mli 2.5 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
iO.ml 6.9 KB 2997   7 years sacerdot New extraction.
iO.mli 2.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
iOMonad.ml 18.6 KB 2997   7 years sacerdot New extraction.
iOMonad.mli 9.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
jmeq.ml 3.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
jmeq.mli 1.7 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
joint.ml 110.7 KB 3001   7 years sacerdot New extraction.
joint.mli 54.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
joint_fullexec.ml 3.2 KB 2968   7 years sacerdot The initial status memory was not really initialized. Now it is.
joint_fullexec.mli 1.5 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
joint_LTL_LIN.ml 13.4 KB 3001   7 years sacerdot New extraction.
joint_LTL_LIN.mli 6.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
joint_LTL_LIN_semantics.ml 7.7 KB 2997   7 years sacerdot New extraction.
joint_LTL_LIN_semantics.mli 2.3 KB 2997   7 years sacerdot New extraction.
joint_printer.ml 60.8 KB 2996   7 years sacerdot Printing of graphs now starts from the entry point.
joint_printer.mli 25.8 KB 2996   7 years sacerdot Printing of graphs now starts from the entry point.
joint_semantics.ml 113.0 KB 3001   7 years sacerdot New extraction.
joint_semantics.mli 52.3 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
label.ml 26.0 KB 3001   7 years sacerdot New extraction.
label.mli 2.7 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
labelledObjects.ml 2.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
labelledObjects.mli 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
lIN.ml 2.0 KB 3001   7 years sacerdot New extraction.
lIN.mli 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lIN_printer.ml 1.3 KB 2995   7 years sacerdot The lIN_printer extracted.
lIN_printer.mli 1.0 KB 2995   7 years sacerdot The lIN_printer extracted.
lIN_semantics.ml 1.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lIN_semantics.mli 1.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
linearise.ml 11.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
linearise.mli 2.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lINToASM.ml 62.9 KB 3001   7 years sacerdot New extraction.
lINToASM.mli 9.2 KB 2986   7 years sacerdot New extraction.
list.ml 9.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
list.mli 3.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
listb.ml 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
listb.mli 477 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
listb_extra.ml 232 bytes 2730   7 years sacerdot Exported again.
listb_extra.mli 232 bytes 2730   7 years sacerdot Exported again.
lists.ml 2.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
lists.mli 945 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
liveness.ml 15.1 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
liveness.mli 2.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
logic.ml 6.3 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
logic.mli 2.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
lTL.ml 4.1 KB 3001   7 years sacerdot New extraction.
lTL.mli 2.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTL_printer.ml 1.3 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTL_printer.mli 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTL_semantics.ml 1.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTL_semantics.mli 1.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTLToLIN.ml 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
lTLToLIN.mli 982 bytes 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
measurable.ml 20.6 KB 2997   7 years sacerdot New extraction.
measurable.mli 8.8 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
memoryInjections.ml 5.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
memoryInjections.mli 2.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
memProperties.ml 1.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
memProperties.mli 1016 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
MODIFIED_BY_HAND 48 bytes 2966   7 years sacerdot Modified by hand files (to improve a little bit the performance).
monad.ml 20.1 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
monad.mli 9.5 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
nat.ml 3.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
nat.mli 1.2 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
option.ml 1.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
option.mli 366 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
order.ml 2.6 KB 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
order.mli 968 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pointers.ml 11.0 KB 3001   7 years sacerdot New extraction.
pointers.mli 4.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
policy.ml 4.7 KB 3001   7 years sacerdot New extraction.
policy.mli 1.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
policyFront.ml 27.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
policyFront.mli 2.6 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
policyStep.ml 7.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
policyStep.mli 864 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
positive.ml 12.1 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
positive.mli 3.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
positiveMap.ml 12.7 KB 2827   7 years sacerdot Everything extracted again.
positiveMap.mli 4.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
preamble.ml 64 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
preIdentifiers.ml 6.7 KB 2827   7 years sacerdot Everything extracted again.
preIdentifiers.mli 2.8 KB 2649   7 years sacerdot
PROBLEMS 499 bytes 2836   7 years sacerdot
proper.ml 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
proper.mli 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pts.ml 35 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
pts.mli 35 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
registers.ml 645 bytes 2649   7 years sacerdot
registers.mli 564 bytes 2649   7 years sacerdot
registerSet.ml 11.6 KB 3001   7 years sacerdot New extraction.
registerSet.mli 6.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
relations.ml 324 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
relations.mli 286 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
rTL.ml 9.0 KB 3001   7 years sacerdot New extraction.
rTL.mli 3.4 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTL_printer.ml 1.3 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTL_printer.mli 1.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTL_semantics.ml 28.0 KB 3001   7 years sacerdot New extraction.
rTL_semantics.mli 7.7 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
rTLabs_abstract.ml 19.3 KB 3001   7 years sacerdot New extraction.
rTLabs_abstract.mli 7.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
rTLabs_classified_system.ml 1.9 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTLabs_classified_system.mli 1.2 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTLabs_semantics.ml 85.1 KB 3001   7 years sacerdot New extraction.
rTLabs_semantics.mli 9.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
rTLabs_syntax.ml 30.0 KB 3001   7 years sacerdot New extraction.
rTLabs_syntax.mli 18.2 KB 2997   7 years sacerdot New extraction.
rTLabs_traces.ml 90.7 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTLabs_traces.mli 34.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
rTLabsToRTL.ml 49.3 KB 3006   7 years sacerdot New extraction, bugs fixed.
rTLabsToRTL.mli 10.8 KB 3006   7 years sacerdot New extraction, bugs fixed.
rTLToERTL.ml 17.8 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
rTLToERTL.mli 3.9 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
russell.ml 104 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
russell.mli 104 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
semantics.ml 9.6 KB 3001   7 years sacerdot New extraction.
semantics.mli 5.0 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
semanticsUtils.ml 28.3 KB 3001   7 years sacerdot New extraction.
semanticsUtils.mli 13.7 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
setoids.ml 2.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
setoids.mli 1.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
sets.ml 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
sets.mli 81 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
simplifyCasts.ml 28.4 KB 3001   7 years sacerdot New extraction.
simplifyCasts.mli 4.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
smallstep.ml 16.8 KB 3001   7 years sacerdot New extraction.
smallstep.mli 7.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
smallstepExec.ml 21.5 KB 2997   7 years sacerdot New extraction.
smallstepExec.mli 10.2 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
stacksize.ml 8.5 KB 2997   7 years sacerdot New extraction.
stacksize.mli 3.7 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
star.ml 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
star.mli 97 bytes 2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
state.ml 1.1 KB 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
state.mli 539 bytes 2717   7 years sacerdot Extracted code for the whole compiler. The space cost model is not …
status.ml 250.9 KB 2999   7 years sacerdot code_memory added to labelled_object_code to avoid recomputing it …
status.mli 16.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
statusProofs.ml 599 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
statusProofs.mli 599 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
string.ml 890 bytes 2649   7 years sacerdot
string.mli 350 bytes 2649   7 years sacerdot
structuredTraces.ml 80.4 KB 2997   7 years sacerdot New extraction.
structuredTraces.mli 36.5 KB 2873   7 years sacerdot Extracted again.
switchRemoval.ml 23.2 KB 3001   7 years sacerdot New extraction.
switchRemoval.mli 7.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
toCminor.ml 94.4 KB 3001   7 years sacerdot New extraction.
toCminor.mli 15.2 KB 2960   7 years sacerdot New extraction, it diverges in RTL execution now.
toRTLabs.ml 54.6 KB 3001   7 years sacerdot New extraction.
toRTLabs.mli 22.0 KB 2997   7 years sacerdot New extraction.
traces.ml 24.6 KB 3001   7 years sacerdot New extraction.
traces.mli 9.7 KB 2997   7 years sacerdot New extraction.
translateUtils.ml 29.0 KB 3001   7 years sacerdot New extraction.
translateUtils.mli 14.2 KB 2981   7 years sacerdot New extraction after code simplification.
typeComparison.ml 7.8 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
typeComparison.mli 1.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
types.ml 14.1 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
types.mli 5.9 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
uses.ml 3.5 KB 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
uses.mli 1022 bytes 2951   7 years sacerdot New extraction. Novely: a pre-main is used in the back-end. …
util.ml 21.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
util.mli 6.4 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
utilBranch.ml 445 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
utilBranch.mli 361 bytes 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
values.ml 13.8 KB 2997   7 years sacerdot New extraction.
values.mli 3.3 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
vector.ml 14.8 KB 2775   7 years sacerdot The compiler now computes also the stack cost model.
vector.mli 5.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
z.ml 7.6 KB 2827   7 years sacerdot Everything extracted again.
z.mli 2.0 KB 2773   7 years sacerdot 1. everything extracted again after all bugs in Matita's extraction …
Note: See TracBrowser for help on using the repository browser.