X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2F.depend;h=bb3e16d8e8bc73402a1f0b0263114ed06b97aea3;hb=6e01bb1ae52fe45ce77a7f950efb5feb295e82b1;hp=b52cdc6b3b99776b086fd07a406966bf3b87df3e;hpb=936f80cf031a7b034dd70fef49abb90e69f2e680;p=helm.git diff --git a/components/tactics/.depend b/components/tactics/.depend index b52cdc6b3..bb3e16d8e 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -31,7 +31,6 @@ 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 @@ -63,8 +62,6 @@ 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 @@ -73,6 +70,8 @@ autoCache.cmo: universe.cmi autoCache.cmi autoCache.cmx: universe.cmx autoCache.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi +closeCoercionGraph.cmo: closeCoercionGraph.cmi +closeCoercionGraph.cmx: closeCoercionGraph.cmi paramodulation/subst.cmo: paramodulation/subst.cmi paramodulation/subst.cmx: paramodulation/subst.cmi paramodulation/equality.cmo: paramodulation/utils.cmi \ @@ -211,7 +210,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi -declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ +declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \ declarative.cmi -declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \ +declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \ declarative.cmi