From 6caf8b877e44862b21104236423c23972166cdd7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 11:14:03 +0100
Subject: Fix the comment of Refine.refine

---
 proofs/proofview.mli | 4 ++--
 1 file 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} *)
-- 
cgit v1.2.3