X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2F.depend;h=b52cdc6b3b99776b086fd07a406966bf3b87df3e;hb=936f80cf031a7b034dd70fef49abb90e69f2e680;hp=07d7fc08b60772bc58d7238de7f06b5e14dcff3f;hpb=ce5018fb3004d79fd16301dfc0fd9370d59ba4fc;p=helm.git diff --git a/components/tactics/.depend b/components/tactics/.depend index 07d7fc08b..b52cdc6b3 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -17,6 +17,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi +compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi @@ -30,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi @@ -61,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +closeCoercionGraph.cmo: closeCoercionGraph.cmi +closeCoercionGraph.cmx: closeCoercionGraph.cmi universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi autoTypes.cmo: autoTypes.cmi @@ -107,6 +111,10 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ variousTactics.cmi +compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \ + closeCoercionGraph.cmi compose.cmi +compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \ + closeCoercionGraph.cmx compose.cmi introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ @@ -196,13 +204,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \ primitiveTactics.cmi negationTactics.cmi inversion.cmi \ introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ - auto.cmi tactics.cmi + compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx negationTactics.cmx inversion.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ - auto.cmx tactics.cmi + compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \