diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 079baa3ef..7809dbf48 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -95,6 +95,14 @@ val try_intros_until : (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings destruction_arg -> unit Proofview.tactic |