diff options
| author | Maxime Dénès | 2018-01-25 13:37:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-25 13:37:59 +0100 |
| commit | 05e0b45a254ab37e912e677d732aca20389263a8 (patch) | |
| tree | f14d18bcdc70512849589a727168c04c6a50084a | |
| parent | 2e798fb83db743ce44350af6f7f9442811f374ad (diff) | |
| parent | a6a1cf208ddc89b06b67f13f4291dc944534684a (diff) | |
Merge PR #6620: Fix #6591: anomaly when using selectors outside of a proof.
| -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 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 |