diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-19 11:12:06 +0100 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-22 11:09:12 +0100 |
| commit | a6a1cf208ddc89b06b67f13f4291dc944534684a (patch) | |
| tree | 9575cd4cce9a2f2f970a5298e5c3ac3cfc8bb788 /proofs | |
| parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) | |
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.
Diffstat (limited to 'proofs')
| -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 |