X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2F.depend;h=6c23fc90985a7ab63ef41d3b7df4b85a4779f8d2;hb=4480f2625fce077f7389dde595920d25748820eb;hp=c8317fca41aa1c00c0a0900425c5b840f3b85c9b;hpb=06b128f1107fd579a696b83b2f8255f83ab29a92;p=helm.git

diff --git a/components/tactics/.depend b/components/tactics/.depend
index c8317fca4..6c23fc909 100644
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -31,7 +31,7 @@ fourierR.cmi: proofEngineTypes.cmi
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 tactics.cmi: universe.cmi proofEngineTypes.cmi 
-declarative.cmi: proofEngineTypes.cmi 
+declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -53,9 +53,9 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmi \
 proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
     proofEngineStructuralRules.cmi 
 primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineHelpers.cmi primitiveTactics.cmi 
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi 
 primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineHelpers.cmx primitiveTactics.cmi 
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi 
 hashtbl_equiv.cmo: hashtbl_equiv.cmi 
 hashtbl_equiv.cmx: hashtbl_equiv.cmi 
 metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
@@ -112,12 +112,12 @@ introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     introductionTactics.cmi 
-eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
-    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
-    primitiveTactics.cmi eliminationTactics.cmi 
-eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
-    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
-    primitiveTactics.cmx eliminationTactics.cmi 
+eliminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
+    proofEngineTypes.cmi proofEngineStructuralRules.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi eliminationTactics.cmi 
+eliminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
+    proofEngineTypes.cmx proofEngineStructuralRules.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx eliminationTactics.cmi 
 negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \
     primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi 
 negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \
@@ -204,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
     fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
     eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
     tactics.cmi 
-declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
-declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
     declarative.cmi