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 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 0a6435195..47b9b406d 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 -> -- cgit v1.2.3