X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FMakefile;h=0b3fd06b1ad83eec655a95feb0561ca14049aad8;hb=795c7a7a2f45650204e6d5a5974a0eedec6af7af;hp=44c9887f77da93bef40a146ef523bb8a09203f9a;hpb=7e755543523fd1dc050e062b277996b0c9f4752e;p=helm.git

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 44c9887f7..0b3fd06b1 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -14,13 +14,22 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA
 all: gTopLevel
 opt: gTopLevel.opt
 
-DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \
-          cic2acic.ml cic2acic.mli logicalOperations.ml sequentPp.ml \
-          mquery.mli mquery.ml gTopLevel.ml
-
-TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \
-               cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \
-               mquery.cmo gTopLevel.cmo
+DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \
+	  proofEngineReduction.ml proofEngineReduction.mli \
+          proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
+          primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
+	  proofEngine.ml proofEngine.mli \
+          doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
+          cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
+          logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \
+          mQueryGenerator.ml gTopLevel.ml
+
+TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
+			   proofEngineReduction.cmo proofEngineStructuralRules.cmo \
+			   primitiveTactics.cmo ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \
+               doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
+               logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \
+	           gTopLevel.cmo
 
 depend:
 	$(OCAMLDEP) $(DEPOBJS) > .depend