X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend;h=29482257cd6ea83b08282279d0d204da14d4e2be;hb=75514fe2207992ebc549822a7cbd5d37688690ac;hp=e7aa8868db7954a8b421029927740cfc3bedf0be;hpb=7cb22a7f8107a6cde0b77b7879e04f586a347102;p=helm.git diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index e7aa8868d..29482257c 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,19 +1,11 @@ -proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi -proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi -hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi -universe.cmi: autoTypes.cmi: proofEngineTypes.cmi -autoCache.cmi: -paramodulation/utils.cmi: -closeCoercionGraph.cmi: -paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -24,7 +16,8 @@ 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 +automationCache.cmi: universe.cmi paramodulation/saturation.cmi \ + paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi @@ -34,13 +27,10 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi -inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi -fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi -history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi @@ -119,9 +109,9 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/indexing.cmx paramodulation/founif.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi automationCache.cmo: universe.cmi paramodulation/saturation.cmi \ - automationCache.cmi + paramodulation/equality.cmi automationCache.cmi automationCache.cmx: universe.cmx paramodulation/saturation.cmx \ - automationCache.cmi + paramodulation/equality.cmx automationCache.cmi variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ variousTactics.cmi variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \