From 843aa67736fad6efae3be67dba909164394674e9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2012 00:00:33 +0000
Subject: Backtrack: add support for the "Proof c." syntax (fix #2832)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15528 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 6 ++++--
 1 file 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
-- 
cgit v1.2.3