diff options
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index cfdcde36e..1932a306c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -33,7 +33,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr (** A variant of [refine] which assumes exactly one goal under focus *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> - [ `NF ] Proofview.Goal.t -> 'a tactic + Proofview.Goal.t -> 'a tactic (** The general version of refine. *) (** {7 Helper functions} *) |