X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Ftactics.ml;h=82c343085a0c0b4ec38e35693db54acfebd4a8b5;hb=46bde81a59b45bedd6d859450decfc2263d92d7e;hp=c34355b8ea21fd382dcfa08c9d0e9cc728056ab7;hpb=9a651e3b71b51dddba23519ab567faf5cf474edd;p=helm.git diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index c34355b8e..82c343085 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -30,6 +30,7 @@ let apply = PrimitiveTactics.apply_tac let applyS = Auto.applyS_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac +let cases_intros = PrimitiveTactics.cases_intros_tac let change = ReductionTactics.change_tac let clear = ProofEngineStructuralRules.clear let clearbody = ProofEngineStructuralRules.clearbody