- | TacticAst.Right _ -> Tactics.right
- | TacticAst.Ring _ -> Tactics.ring
- | TacticAst.Split _ -> Tactics.split
- | TacticAst.Symmetry _ -> Tactics.symmetry
- | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
- | TacticAst.Apply (_, term) -> Tactics.apply term
- | TacticAst.Absurd (_, term) -> Tactics.absurd term
- | TacticAst.Exact (_, term) -> Tactics.exact term
- | TacticAst.Cut (_, term) -> Tactics.cut term
- | TacticAst.Elim (_, term, _) ->
- (* TODO Zack implement "using" argument *)
- (* old: Tactics.elim_intros_simpl term *)
- Tactics.elim_intros term
- | TacticAst.ElimType (_, term) -> Tactics.elim_type term
- | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
- | TacticAst.Auto (_,depth) ->
-(* AutoTactic.auto_tac ~num (MatitaDb.instance ()) *)
- AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) ()
- | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
-(*
- (* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
- | TacticAst.Change of 'term * 'term * 'ident option
- | TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Fold of reduction_kind * 'term
- | TacticAst.Injection of 'ident
- | TacticAst.Replace_pattern of 'term pattern * 'term
-*)