X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend.opt;h=a9f6e372e5c54d957113032e68338994d193447a;hb=86ff79af764c2a434fdf38ea344ab722811981c8;hp=a278f6f0836f66a12becb40648662f44c709a1e6;hpb=13bfd154ade0996d34e7e723398ac7ab76a51717;p=helm.git diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index a278f6f08..a9f6e372e 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -1,11 +1,19 @@ +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 @@ -25,10 +33,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.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: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi