- "linear" flag added to lapply (automatic clearing)

[helm.git] / helm / software / components / tactics / .depend

diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index e94cfa5ab2f333e2ef303ae40cf80d6f288807b3..743811ceb5d9d315e622ff08c7adffff53b62d5d 100644 (file)
--- 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