From a6a1cf208ddc89b06b67f13f4291dc944534684a Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 19 Jan 2018 11:12:06 +0100
Subject: Fix #6591: anomaly when using selectors outside of a proof.

When asking for a hint about bullets, we check
that there is an ongoing proof.
---
 proofs/proof_global.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d04bdb6521..fc94a10132 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -485,7 +485,10 @@ let update_global_env () =
 (* XXX: Bullet hook, should be really moved elsewhere *)
 let _ =
   let hook n =
-    let prf = give_me_the_proof () in
-    (Proof_bullet.suggest prf) in
+    try
+      let prf = give_me_the_proof () in
+      (Proof_bullet.suggest prf)
+    with NoCurrentProof -> mt ()
+  in
   Proofview.set_nosuchgoals_hook hook
 
-- 
cgit v1.2.3