From: Enrico Tassi Date: Thu, 14 Dec 2006 18:15:39 +0000 (+0000) Subject: ... X-Git-Tag: 0.4.95@7852~732 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=378a122bd40f832581ee3e82cc428584b6579a57;p=helm.git ... --- diff --git a/components/tactics/.depend b/components/tactics/.depend index c8317fca4..dbccfe6d7 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -31,7 +31,7 @@ fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: universe.cmi proofEngineTypes.cmi -declarative.cmi: proofEngineTypes.cmi +declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi @@ -112,12 +112,12 @@ introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ introductionTactics.cmi -eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ - proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ - primitiveTactics.cmi eliminationTactics.cmi -eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ - proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ - primitiveTactics.cmx eliminationTactics.cmi +eliminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ + proofEngineTypes.cmi proofEngineStructuralRules.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi eliminationTactics.cmi +eliminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ + proofEngineTypes.cmx proofEngineStructuralRules.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx eliminationTactics.cmi negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \ primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \ @@ -204,7 +204,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \ fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \ tactics.cmi -declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \ +declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi -declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \ +declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ declarative.cmi