renamed Http_client to Http_user_agent to avoid clashes with Gerd's

[helm.git] / helm / gTopLevel / Makefile.in

diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in
index 74b93230b833d1ecae95aa24d538f7d51524bbdb..4b44c3418cb0616a3430096a30dd05222c7aa7ca 100644 (file)
--- a/helm/gTopLevel/Makefile.in
+++ b/helm/gTopLevel/Makefile.in
@@ -7,11 +7,11 @@ TEST_REQUIRES = \
        helm-tactics \
        helm-cic_transformations \
        helm-cic_textual_parser2 \
-       helm-cic_textual_parser \
-       helm-tex_cic_textual_parser \
+       helm-xmldiff \
        lablgtk2 \
        mathml-editor \
-       lablgtkmathview
+       lablgtkmathview \
+       dbi.mysql
 
 REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
 
@@ -40,11 +40,9 @@ stop:
 INTERFACE_FILES = \
        proofEngine.mli \
        logicalOperations.mli \
-       oldDisambiguate.mli \
        disambiguatingParser.mli \
        termEditor.mli \
        texTermEditor.mli \
-       xmlDiff.mli \
        chosenTransformer.mli \
        termViewer.mli \
        invokeTactics.mli \
@@ -58,7 +56,6 @@ DEPOBJS = \
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
 TESTOBJS = \
-       oldDisambiguate.cmo \
        disambiguatingParser.cmo \
        batchParser.cmo
 REGTESTOBJS = $(TESTOBJS) regtest.cmo
@@ -137,6 +134,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 =