]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/.depend
- init_cache_and_tables rewritten using the automation_cache
[helm.git] / helm / software / components / tactics / .depend
index 9dca5c5fbeb7d5098d990edb4c241476bccb73da..e7aa8868db7954a8b421029927740cfc3bedf0be 100644 (file)
@@ -31,7 +31,7 @@ introductionTactics.cmi: proofEngineTypes.cmi
 eliminationTactics.cmi: proofEngineTypes.cmi 
 negationTactics.cmi: proofEngineTypes.cmi 
 equalityTactics.cmi: proofEngineTypes.cmi 
-auto.cmi: universe.cmi proofEngineTypes.cmi 
+auto.cmi: proofEngineTypes.cmi automationCache.cmi 
 destructTactic.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 inversion_principle.cmi: 
@@ -42,8 +42,8 @@ fourierR.cmi: proofEngineTypes.cmi
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 history.cmi: 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi 
-declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi 
+tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi 
+declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -118,9 +118,9 @@ 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.cmo: universe.cmi paramodulation/saturation.cmi \
     automationCache.cmi 
-automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
+automationCache.cmx: universe.cmx paramodulation/saturation.cmx \
     automationCache.cmi 
 variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     variousTactics.cmi 
@@ -155,13 +155,13 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
 auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/saturation.cmi \
     proofEngineTypes.cmi proofEngineReduction.cmi proofEngineHelpers.cmi \
     primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
-    equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
-    autoCache.cmi auto.cmi 
+    equalityTactics.cmi paramodulation/equality.cmi automationCache.cmi \
+    autoTypes.cmi autoCache.cmi auto.cmi 
 auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/saturation.cmx \
     proofEngineTypes.cmx proofEngineReduction.cmx proofEngineHelpers.cmx \
     primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
-    equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
-    autoCache.cmx auto.cmi 
+    equalityTactics.cmx paramodulation/equality.cmx automationCache.cmx \
+    autoTypes.cmx autoCache.cmx auto.cmi 
 destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
     primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \