diff options
author | 2016-01-08 20:29:37 +0100 | |
---|---|---|
committer | 2016-01-08 21:00:14 +0100 | |
commit | 418dceeea548a40c6e00b09aa99267a82949c70c (patch) | |
tree | e82a08d96fc453dc3745314c000543703a3fea36 /tactics/ftactic.mli | |
parent | 6599e31f04b6e8980de72e9d3913b70c04b6698c (diff) |
Monotonizing Ftactic.
Diffstat (limited to 'tactics/ftactic.mli')
-rw-r--r-- | tactics/ftactic.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli index a20d8a9c3..f0466341f 100644 --- a/tactics/ftactic.mli +++ b/tactics/ftactic.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Proofview.Notations + (** Potentially focussing tactics *) type +'a focus @@ -37,14 +39,19 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : (([ `NF ], 'r) Proofview.Goal.t -> 'a t) -> 'a t +val nf_enter : ([ `NF ], 'a t) enter -> 'a t (** Enter a goal. The resulting tactic is focussed. *) -(** FIXME: Should be polymorphic over the stage. *) -val enter : (([ `LZ ], 'r) Proofview.Goal.t -> 'a t) -> 'a t +val enter : ([ `LZ ], 'a t) enter -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) -(** FIXME: Should be polymorphic over the stage. *) + +val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t +(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *) + +val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t +(** Enter a goal, without evar normalization and put back an evarmap. The + resulting tactic is focussed. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an |