]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/Makefile.in
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / Makefile.in
index 42dd44be1f8f29971aceddcb33846da36806a712..b64716cc2663d5a9cfc92c99c4fdca7d537cce49 100644 (file)
@@ -2,16 +2,16 @@ BIN_DIR = /usr/local/bin
 
 TEST_REQUIRES = \
        helm-registry \
-       helm-mathql_interpreter \
-       helm-mathql_generator \
        helm-tactics \
        helm-cic_transformations \
        helm-cic_textual_parser2 \
+       helm-mathql_interpreter \
+       helm-mathql_generator \
        helm-xmldiff \
        lablgtk2 \
        mathml-editor \
        lablgtkmathview \
-       dbi.mysql
+       mysql
 
 REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
 
@@ -43,7 +43,6 @@ INTERFACE_FILES = \
        disambiguatingParser.mli \
        termEditor.mli \
        texTermEditor.mli \
-       chosenTransformer.mli \
        termViewer.mli \
        invokeTactics.mli \
        hbugs.mli \
@@ -134,6 +133,10 @@ librarytest: testlibrary
        ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
 librarytest.opt: testlibrary.opt
        ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
+typecheck_uri: typecheck_uri.ml
+       $(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
+typecheck_uri.opt: typecheck_uri.ml
+       $(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
 
 MAIN = ./gTopLevel
 ARGS =