X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend;h=10862a5b016c7bb78694e7e44ecb769072472c39;hb=d8f4d935054a6f9fff6de0c171dc4a181389219e;hp=4769431a4a7badfa04ca1ee85870af68667d3503;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 4769431a4..10862a5b0 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -120,12 +120,16 @@ discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi -inversion.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \ - inversion.cmi -inversion.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \ - inversion.cmi +inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + equalityTactics.cmi inversion.cmi +inversion.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + equalityTactics.cmx inversion.cmi +inversion_principle.cmo: tacticals.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi inversion.cmi inversion_principle.cmi +inversion_principle.cmx: tacticals.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx inversion.cmx inversion_principle.cmi ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \