From c25a2152b1ebb7e9833db7c705e257068d89057a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 May 2004 08:56:50 +0000 Subject: [PATCH] * tactics/Makefile fixed (to remove duplicate .mli files) * .depend regenerated --- helm/ocaml/tactics/.depend | 19 +++++++++++++------ helm/ocaml/tactics/Makefile | 1 - 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index d1863019c..3a60f60ac 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -1,3 +1,4 @@ +filter_auto.cmi: newConstraints.cmi proofEngineHelpers.cmi: proofEngineTypes.cmo tacticals.cmi: proofEngineTypes.cmo reductionTactics.cmi: proofEngineTypes.cmo @@ -13,6 +14,12 @@ discriminationTactics.cmi: proofEngineTypes.cmo ring.cmi: proofEngineTypes.cmo fourierR.cmi: proofEngineTypes.cmo statefulProofEngine.cmi: proofEngineTypes.cmo +newConstraints.cmo: newConstraints.cmi +newConstraints.cmx: newConstraints.cmi +match_concl.cmo: newConstraints.cmi match_concl.cmi +match_concl.cmx: newConstraints.cmx match_concl.cmi +filter_auto.cmo: newConstraints.cmi filter_auto.cmi +filter_auto.cmx: newConstraints.cmx filter_auto.cmi proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi @@ -35,10 +42,10 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi -tacticChaser.cmo: match_concl.cmi primitiveTactics.cmi proofEngineTypes.cmo \ - tacticChaser.cmi -tacticChaser.cmx: match_concl.cmx primitiveTactics.cmx proofEngineTypes.cmx \ - tacticChaser.cmi +tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \ + primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi +tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \ + primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ @@ -83,5 +90,5 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ tacticals.cmx fourierR.cmi -statefulProofEngine.cmo: statefulProofEngine.cmi -statefulProofEngine.cmx: statefulProofEngine.cmi +statefulProofEngine.cmo: proofEngineTypes.cmo statefulProofEngine.cmi +statefulProofEngine.cmx: proofEngineTypes.cmx statefulProofEngine.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 36c81117f..0cf06c578 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -6,7 +6,6 @@ REQUIRES = \ INTERFACE_FILES = \ newConstraints.mli match_concl.mli filter_auto.mli\ proofEngineReduction.mli proofEngineHelpers.mli \ - newConstraints.mli match_concl.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli tacticChaser.mli variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ -- 2.39.2