From: Claudio Sacerdoti Coen Date: Tue, 28 Jan 2003 17:30:33 +0000 (+0000) Subject: Fixed. It was no more working since the move of the tactics under the ocaml X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ab573d2f8ee8d82771ef7a8a925d9449cf225ce9;p=helm.git Fixed. It was no more working since the move of the tactics under the ocaml repository. --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 6989c187b..b27f702c0 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,81 +1,7 @@ xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi -proofEngineHelpers.cmo: proofEngineHelpers.cmi -proofEngineHelpers.cmx: proofEngineHelpers.cmi -proofEngineReduction.cmo: proofEngineReduction.cmi -proofEngineReduction.cmx: proofEngineReduction.cmi -proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ - proofEngineStructuralRules.cmi -proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ - proofEngineStructuralRules.cmi -proofEngineStructuralRules.cmi: proofEngineTypes.cmo -tacticals.cmo: proofEngineTypes.cmo tacticals.cmi -tacticals.cmx: proofEngineTypes.cmx tacticals.cmi -tacticals.cmi: proofEngineTypes.cmo -reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi -reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi -reductionTactics.cmi: proofEngineTypes.cmo -primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \ - primitiveTactics.cmi -primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ - primitiveTactics.cmi -primitiveTactics.cmi: proofEngineTypes.cmo -variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmo tacticals.cmi variousTactics.cmi -variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx tacticals.cmx variousTactics.cmi -variousTactics.cmi: proofEngineTypes.cmo -introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \ - introductionTactics.cmi -introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ - introductionTactics.cmi -introductionTactics.cmi: proofEngineTypes.cmo -eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ - proofEngineTypes.cmo tacticals.cmi eliminationTactics.cmi -eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ - proofEngineTypes.cmx tacticals.cmx eliminationTactics.cmi -eliminationTactics.cmi: proofEngineTypes.cmo -negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \ - proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi -negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \ - proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi -negationTactics.cmi: proofEngineTypes.cmo -equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \ - tacticals.cmi equalityTactics.cmi -equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \ - proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ - tacticals.cmx equalityTactics.cmi -equalityTactics.cmi: proofEngineTypes.cmo -ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \ - ring.cmi -ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ - proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ - ring.cmi -ring.cmi: proofEngineTypes.cmo -fourierR.cmo: equalityTactics.cmi fourier.cmo primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \ - tacticals.cmi fourierR.cmi -fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ - proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ - tacticals.cmx fourierR.cmi -fourierR.cmi: proofEngineTypes.cmo -proofEngine.cmo: eliminationTactics.cmi equalityTactics.cmi fourierR.cmi \ - introductionTactics.cmi negationTactics.cmi primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \ - ring.cmi variousTactics.cmi proofEngine.cmi -proofEngine.cmx: eliminationTactics.cmx equalityTactics.cmx fourierR.cmx \ - introductionTactics.cmx negationTactics.cmx primitiveTactics.cmx \ - proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ - ring.cmx variousTactics.cmx proofEngine.cmi -proofEngine.cmi: proofEngineTypes.cmo +proofEngine.cmo: proofEngine.cmi +proofEngine.cmx: proofEngine.cmi doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index e919c6a24..cf12d3121 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,11 +1,12 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ - helm-xml gdome2-xslt helm-cic_unification helm-mathql \ + helm-xml gdome2-xslt helm-cic_unification helm-tactics helm-mathql \ helm-mathql_interpreter -PREDICATES = "gnome,init" +PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLFIND = ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) OCAMLDEP = ocamldep -pp camlp4o LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) @@ -14,31 +15,18 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA all: gTopLevel opt: gTopLevel.opt -DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ - proofEngineReduction.ml proofEngineReduction.mli \ - proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ - tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \ - primitiveTactics.ml primitiveTactics.mli variousTactics.ml \ - variousTactics.mli introductionTactics.ml introductionTactics.mli \ - eliminationTactics.ml eliminationTactics.mli negationTactics.ml \ - negationTactics.mli equalityTactics.ml equalityTactics.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 \ - mQueryLevels.ml mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml\ - disambiguate.ml disambiguate.mli gTopLevel.ml - -TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ - proofEngineReduction.cmo proofEngineStructuralRules.cmo \ - tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \ - variousTactics.cmo introductionTactics.cmo \ - eliminationTactics.cmo negationTactics.cmo equalityTactics.cmo \ - ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ - doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \ - mQueryLevels2.cmo mQueryGenerator.cmo disambiguate.cmo \ - gTopLevel.cmo +DEPOBJS = \ + xml2Gdome.ml xml2Gdome.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 mQueryLevels.ml \ + mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml disambiguate.ml \ + disambiguate.mli gTopLevel.ml + +TOPLEVELOBJS = \ + xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \ + cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \ + mQueryLevels2.cmo mQueryGenerator.cmo disambiguate.cmo gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend