diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-24 04:38:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f (patch) | |
| tree | edfad66c97aeea8b7e4aad4aba395aacb2175a3c /tactics/tactics.mli | |
| parent | 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 (diff) | |
[api] Misctypes removal: tactic flags.
We move the "flag types" to its use place, and mark some arguments
with named parameters better.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 086442e42..8d4302450 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -18,7 +18,6 @@ open Clenv open Redexpr open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -91,6 +90,11 @@ val intros_clearing : bool list -> unit Proofview.tactic val try_intros_until : (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) |