X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftactics.ml;h=4676d2d10c6217214abae20e46a444afcc86058c;hb=cdb7b3dcac3ff13a18ce67878ab7aec2302a9a77;hp=4d52725891e04f5e2e24ca2d4ec8ae367366fe40;hpb=8c19127e7ee6c71006838f89583a3283451b664c;p=helm.git diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 4d5272589..4676d2d10 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -27,6 +27,7 @@ let absurd = NegationTactics.absurd_tac let apply = PrimitiveTactics.apply_tac +let applyS = AutoTactic.applyS_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac let change = ReductionTactics.change_tac @@ -66,6 +67,7 @@ let ring = Ring.ring_tac let set_goal = ProofEngineStructuralRules.set_goal let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac +let subst = EqualityTactics.subst_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let unfold = ReductionTactics.unfold_tac