X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend;h=29482257cd6ea83b08282279d0d204da14d4e2be;hb=75514fe2207992ebc549822a7cbd5d37688690ac;hp=a278f6f0836f66a12becb40648662f44c709a1e6;hpb=ffdd3ddd6ce10a5fa0729ab407647bd46c44b9d8;p=helm.git diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index a278f6f08..29482257c 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -16,13 +16,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 ring.cmi: proofEngineTypes.cmi @@ -30,8 +32,8 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.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 @@ -106,6 +108,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 \ @@ -139,13 +145,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 \