diff options
| author | Matthieu Sozeau | 2016-03-14 11:14:03 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-14 11:40:52 +0100 |
| commit | 6caf8b877e44862b21104236423c23972166cdd7 (patch) | |
| tree | afec63b262daf9cdb9c9f91dec04959d95f8accd | |
| parent | 1b984a697076aae9bbdb96efbecbbbec274cbf2a (diff) | |
Fix the comment of Refine.refine
| -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} *) |