Universe is used only locally to tactics/

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

diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index a9f6e372e5c54d957113032e68338994d193447a..9dca5c5fbeb7d5098d990edb4c241476bccb73da 100644 (file)
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -24,6 +24,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \
     paramodulation/equality.cmi 
 paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
     paramodulation/indexing.cmi paramodulation/equality.cmi 
+automationCache.cmi: universe.cmi paramodulation/saturation.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
 compose.cmi: proofEngineTypes.cmi 
 introductionTactics.cmi: proofEngineTypes.cmi 
@@ -117,6 +118,10 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \
     paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
     paramodulation/indexing.cmx paramodulation/founif.cmx \
     paramodulation/equality.cmx paramodulation/saturation.cmi 
+automationCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
+    automationCache.cmi 
+automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
+    automationCache.cmi 
 variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     variousTactics.cmi 
 variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \