From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 May 2004 08:56:50 +0000 (+0000)
Subject: * tactics/Makefile fixed (to remove duplicate .mli files)
X-Git-Tag: V_0_0_9~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c25a2152b1ebb7e9833db7c705e257068d89057a;p=helm.git

* tactics/Makefile fixed (to remove duplicate .mli files)
* .depend regenerated
---

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 \