X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2F.depend;h=d667574faa70f8dce42b1a3c5a69756e00168bfe;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2c6ce4b0f0813c89beb5db925b4e669698231435;hpb=a268d7377c1d4ddae4229f5844125f827325c78a;p=helm.git diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 2c6ce4b0f..d667574fa 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -1,5 +1,6 @@ proofEngineHelpers.cmi: proofEngineTypes.cmi -tacticals.cmi: proofEngineTypes.cmi +continuationals.cmi: proofEngineTypes.cmi +tacticals.cmi: proofEngineTypes.cmi continuationals.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi @@ -13,28 +14,33 @@ equalityTactics.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi +fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi -proofEngineReduction.cmo: proofEngineReduction.cmi -proofEngineReduction.cmx: proofEngineReduction.cmi -proofEngineHelpers.cmo: proofEngineHelpers.cmi -proofEngineHelpers.cmx: proofEngineHelpers.cmi -tacticals.cmo: proofEngineTypes.cmi tacticals.cmi -tacticals.cmx: proofEngineTypes.cmx tacticals.cmi +proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi +proofEngineReduction.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmi +continuationals.cmo: proofEngineTypes.cmi continuationals.cmi +continuationals.cmx: proofEngineTypes.cmx continuationals.cmi +tacticals.cmo: proofEngineTypes.cmi continuationals.cmi tacticals.cmi +tacticals.cmx: proofEngineTypes.cmx continuationals.cmx tacticals.cmi reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ - reductionTactics.cmi + proofEngineHelpers.cmi reductionTactics.cmi reductionTactics.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ - reductionTactics.cmi + proofEngineHelpers.cmx reductionTactics.cmi proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi + proofEngineHelpers.cmi primitiveTactics.cmi primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi + proofEngineHelpers.cmx primitiveTactics.cmi hashtbl_equiv.cmo: hashtbl_equiv.cmi hashtbl_equiv.cmx: hashtbl_equiv.cmi metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ @@ -42,9 +48,11 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi primitiveTactics.cmi variousTactics.cmi + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + variousTactics.cmi variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx primitiveTactics.cmx variousTactics.cmi + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + variousTactics.cmi autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ primitiveTactics.cmi metadataQuery.cmi autoTactic.cmi autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ @@ -54,11 +62,11 @@ introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ introductionTactics.cmi eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ - proofEngineStructuralRules.cmi primitiveTactics.cmi \ - eliminationTactics.cmi + proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi eliminationTactics.cmi eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ - proofEngineStructuralRules.cmx primitiveTactics.cmx \ - eliminationTactics.cmi + proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.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 \ @@ -71,12 +79,12 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi -discriminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ - primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ - eliminationTactics.cmi discriminationTactics.cmi -discriminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ - primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \ - eliminationTactics.cmx discriminationTactics.cmi +discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ + proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \ + equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi +discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ + proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \ + equalityTactics.cmx eliminationTactics.cmx discriminationTactics.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 \ @@ -89,17 +97,25 @@ fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ fourier.cmx equalityTactics.cmx fourierR.cmi +fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi +fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi history.cmo: history.cmi history.cmx: history.cmi statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi ring.cmi reductionTactics.cmi \ - primitiveTactics.cmi negationTactics.cmi introductionTactics.cmi \ - fourierR.cmi equalityTactics.cmi eliminationTactics.cmi \ - discriminationTactics.cmi autoTactic.cmi tactics.cmi -tactics.cmx: variousTactics.cmx ring.cmx reductionTactics.cmx \ - primitiveTactics.cmx negationTactics.cmx introductionTactics.cmx \ - fourierR.cmx equalityTactics.cmx eliminationTactics.cmx \ - discriminationTactics.cmx autoTactic.cmx tactics.cmi +tactics.cmo: variousTactics.cmi tacticals.cmi ring.cmi reductionTactics.cmi \ + proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ + introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ + equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ + autoTactic.cmi tactics.cmi +tactics.cmx: variousTactics.cmx tacticals.cmx ring.cmx reductionTactics.cmx \ + proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ + introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ + equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ + autoTactic.cmx tactics.cmi