X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FMakefile.in;h=b64716cc2663d5a9cfc92c99c4fdca7d537cce49;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=402813f91e157a08a5e929fd28769dafd5e31713;hpb=c6d966bbc276fb0d3bb36ef2945c7bfa31a5ff1b;p=helm.git

diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in
index 402813f91..b64716cc2 100644
--- a/helm/gTopLevel/Makefile.in
+++ b/helm/gTopLevel/Makefile.in
@@ -2,22 +2,22 @@ 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-cic_textual_parser \
-	helm-tex_cic_textual_parser \
+	helm-mathql_interpreter \
+	helm-mathql_generator \
+	helm-xmldiff \
+	lablgtk2 \
 	mathml-editor \
-	lablgtkmathview
+	lablgtkmathview \
+	mysql
 
-REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs
+REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
 
-PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = \
 	-package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread
-OCAMLFIND = ocamlfind
+OCAMLFIND = @OCAMLFIND@
 OCAMLDEBUGOPTIONS = -g
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
 OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
@@ -40,12 +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 \
 	hbugs.mli \
@@ -58,7 +55,6 @@ DEPOBJS = \
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
 TESTOBJS = \
-	oldDisambiguate.cmo \
 	disambiguatingParser.cmo \
 	batchParser.cmo
 REGTESTOBJS = $(TESTOBJS) regtest.cmo
@@ -137,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 =