diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e346a0d566..78a2373952 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -96,6 +96,10 @@ val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings induction_arg -> unit Proofview.tactic +val force_induction_arg : env -> evar_map -> + delayed_open_constr_with_bindings induction_arg -> + constr with_bindings induction_arg + (** Tell if a used hypothesis should be cleared by default or not *) val use_clear_hyp_by_default : unit -> bool |