From b4e1a902910cfab698fd5bdd2e9a18a28944c95e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.ml  | 9 +--------
 engine/proofview.mli | 2 +-
 2 files changed, 2 insertions(+), 9 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 39ef65dab..03148d619 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1072,13 +1072,6 @@ module Goal = struct
     end
     end
 
-  exception NotExactlyOneSubgoal
-  let _ = CErrors.register_handler begin function
-  | NotExactlyOneSubgoal ->
-      CErrors.user_err (Pp.str"Not exactly one subgoal.")
-  | _ -> raise CErrors.Unhandled
-  end
-
   let enter_one f =
     let open Proof in
     Comb.get >>= function
@@ -1090,7 +1083,7 @@ module Goal = struct
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
-    | _ -> tclZERO NotExactlyOneSubgoal
+    | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *)
 
   let goals =
     Pv.get >>= fun step ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index aae25b6f8..3719cacad 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