diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-04 08:33:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-16 15:30:09 +0200 |
| commit | 1a1af4f2119715245b8d4488664a8b57f4bdce08 (patch) | |
| tree | c76d6383b9761ce5042b2062efd381057cdc5600 /proofs/refine.mli | |
| parent | 753248c145cdac846528d809a1f085c18408e17f (diff) | |
Adding variants enter_one and refine_one which assume that exactly one
goal is under focus and which support returning a relevant output.
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index a9798b704..3d140f036 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -30,6 +30,9 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) +val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +(** A generalization of [refine] which assumes exactly one goal under focus *) + (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> |