From 1176d4086b65c79a1d30a55640d3d933fa24a7c1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 25 Jan 2018 16:21:56 +0100
Subject: Proofview: enter_one: add __LOC__ argument to get relevant error msg

The type discipline of the tactic monad does not distinguish between
mono-goal and multi-goal tactics. Unfortunately enter_one "asserts
false" if called on 0 or > 1 goals.  The __LOC__:string argument can
be used to make the error message more helpful (since the backtrace is
pointless inside the monad).

The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..".

The __LOC__ variable is filled in by the OCaml compiler with the current
file name and line number.
---
 engine/proofview.ml  | 5 +++--
 engine/proofview.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 0a64351950..47b9b406d8 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1086,7 +1086,7 @@ module Goal = struct
     end
     end
 
-  let enter_one f =
+  let enter_one ?(__LOC__=__LOC__) f =
     let open Proof in
     Comb.get >>= function
     | [goal] -> begin
@@ -1097,7 +1097,8 @@ module Goal = struct
          let (e, info) = CErrors.push e in
          tclZERO ~info e
       end
-    | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *)
+    | _ ->
+       CErrors.anomaly Pp.(str __LOC__ ++ str " enter_one")
 
   let goals =
     Pv.get >>= fun step ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 59728a2fd1..b02fde3a80 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -499,7 +499,7 @@ module Goal : sig
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
   (** a fatal error otherwise. *)
-  val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
+  val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
       FIXME: encapsulate the level in an existential type. *)
-- 
cgit v1.2.3