Inductive definitions are now interpreted (but records are not interpreted yet).

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

diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
index a9f6e372e5c54d957113032e68338994d193447a..03e70f034e28364a755919b2c6108847d0b466a5 100644 (file)
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -24,13 +24,15 @@ 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 \
+    paramodulation/equality.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
 compose.cmi: proofEngineTypes.cmi 
 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: 
@@ -41,8 +43,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 
@@ -117,6 +119,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: universe.cmi paramodulation/saturation.cmi \
+    paramodulation/equality.cmi automationCache.cmi 
+automationCache.cmx: universe.cmx paramodulation/saturation.cmx \
+    paramodulation/equality.cmx automationCache.cmi 
 variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     variousTactics.cmi 
 variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -150,13 +156,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 \