]> matita.cs.unibo.it Git - helm.git/commit
Implementation of Ocaml extraction (largely ported from Coq).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 2 Feb 2013 00:38:05 +0000 (00:38 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 2 Feb 2013 00:38:05 +0000 (00:38 +0000)
commit7fdb587a1b1764459d2de2e789b30cb180fb172f
tree6f8b84c2bd101383749b6fa752acfb6ac834fb03
parentb3093b1353395ee96d03d9e3771798c3425ff4ac
Implementation of Ocaml extraction (largely ported from Coq).
Note: yet to be thoroughly debugged.

In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc".
13 files changed:
matita/components/METAS/meta.helm-grafite_engine.src
matita/components/METAS/meta.helm-ng_extraction.src [new file with mode: 0644]
matita/components/Makefile
matita/components/grafite_engine/grafiteEngine.ml
matita/components/grafite_engine/grafiteTypes.ml
matita/components/grafite_engine/grafiteTypes.mli
matita/components/ng_kernel/.depend
matita/components/ng_kernel/.depend.opt
matita/components/ng_kernel/Makefile
matita/components/ng_kernel/nCicExtraction.ml [deleted file]
matita/components/ng_kernel/nCicExtraction.mli [deleted file]
matita/components/ng_library/nCicLibrary.mli
matita/matita/matitaEngine.ml