X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend;h=743811ceb5d9d315e622ff08c7adffff53b62d5d;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=e94cfa5ab2f333e2ef303ae40cf80d6f288807b3;hpb=58955ec841575330f0b429033264f9ec7df319f9;p=helm.git

diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index e94cfa5ab..743811ceb 100644
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -87,15 +87,15 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \
     paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
     paramodulation/indexing.cmi 
 paramodulation/saturation.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi primitiveTactics.cmi \
-    paramodulation/inference.cmi paramodulation/indexing.cmi \
-    paramodulation/equality.cmi paramodulation/saturation.cmi 
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \
+    paramodulation/indexing.cmi paramodulation/equality.cmi \
+    paramodulation/saturation.cmi 
 paramodulation/saturation.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx primitiveTactics.cmx \
-    paramodulation/inference.cmx paramodulation/indexing.cmx \
-    paramodulation/equality.cmx paramodulation/saturation.cmi 
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \
+    paramodulation/indexing.cmx paramodulation/equality.cmx \
+    paramodulation/saturation.cmi 
 variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     variousTactics.cmi