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

* .depend regenerated

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index d1863019c7588811e1a255ef1039df42ba7fdc1c..3a60f60ac68568486637681f5bf5521e0a8d93d7 100644 (file)
--- 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 36c81117f5e2d5b6a46ff916f1c69eddf59cc774..0cf06c578f58d9016802fe4a179093886419df73 100644 (file)
--- 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 \