diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index da30513c48..2b3670017f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -373,8 +373,10 @@ let vernac_end_proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - by (Tactics.exact_proof c); - save_named true + let prf = Pfedit.get_current_proof_name () in + by (Tactics.exact_proof c); + save_named true; + Backtrack.mark_unreachable [prf] let vernac_assumption kind l nl= let global = fst kind = Global in |