diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 901cf26e0e..bc68f11ff0 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -499,6 +499,10 @@ module Goal : sig (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : ([ `LZ ], unit tactic) enter -> unit tactic + (** Like {!enter}, but assumes exactly one goal under focus, raising *) + (** an error otherwise. *) + val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } |