diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index dc97e44b6f..7f95a053a8 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -505,9 +505,9 @@ module Refine : sig (** In [refine ?unsafe t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the - new holes created by [t] become the new subgoals. Exception + new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [true] (default) [t] is + tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) (** {7 Helper functions} *) |