diff options
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 *) |