diff options
| -rw-r--r-- | proofs/proof_global.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d04bdb652..fc94a1013 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 |