diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-20 00:34:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-18 13:07:22 +0200 |
| commit | 403af31e3d0bc571acf0a66907277ad839c94df4 (patch) | |
| tree | c35070fc7b51c56db2e313bb824e8cd09e00d2bc /tactics/tactics.mli | |
| parent | a34c17e0e4600d0c466f19b64c3dfb39376981fd (diff) | |
A cleaning phase around delayed induction arg + exporting force_induction_arg.
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 e346a0d56..78a237395 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 |