From 818c49240f2ee6fccd38a556c7e90126606e1837 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Sep 2017 14:45:32 +0200
Subject: Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.

We check that the goal tactic is focussed before calling enter_one.
---
 src/tac2core.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index bbf95c7056..f4486bf0c8 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -116,6 +116,12 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
+let assert_focussed =
+  Proofview.Goal.goals >>= fun gls ->
+  match gls with
+  | [_] -> Proofview.tclUNIT ()
+  | [] | _ :: _ :: _ -> throw err_notfocussed
+
 let pf_apply f =
   Proofview.Goal.goals >>= function
   | [] ->
@@ -682,6 +688,7 @@ end
 
 (** unit -> constr *)
 let () = define0 "goal" begin
+  assert_focussed >>= fun () ->
   Proofview.Goal.enter_one begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
     return (Value.of_constr concl)
-- 
cgit v1.2.3