From b4e1a902910cfab698fd5bdd2e9a18a28944c95e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 15 Jun 2017 21:32:33 +0200
Subject: In enter_one, not having exactly one goal is a fatal error of the
 monad.

Pointed out by PMP.
---
 engine/proofview.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/proofview.mli')

diff --git a/engine/proofview.mli b/engine/proofview.mli
index aae25b6f8f..3719cacad7 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -498,7 +498,7 @@ module Goal : sig
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
-  (** an error otherwise. *)
+  (** a fatal error otherwise. *)
   val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
-- 
cgit v1.2.3