From 5de712460b5bd0794b722ef41f45fa27bc2adc28 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 13 Jan 2006 13:59:15 +0000
Subject: Correction du bug #1055

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7862 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 77312604bc..499190a839 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -345,9 +345,14 @@ let vernac_end_proof = function
      the theories [??] *)
 
 let vernac_exact_proof c =
-  by (Tactics.exact_proof c); 
-  save_named true
-
+  let pts = get_pftreestate () in
+  let pf = top_of_tree (proof_of_pftreestate pts) in
+    if is_leaf_proof pf then 
+      begin by (Tactics.exact_proof c); save_named true end
+    else
+      errorlabstrm "Vernacentries.ExactProof" 
+	(str "Proof can only be used at the beginning of the proof")
+	
 let vernac_assumption kind l =
   List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
 
@@ -563,7 +568,13 @@ let vernac_solve_existential = instantiate_nth_evar_com
 let vernac_set_end_tac tac =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode";
-  if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
+  let pts = get_pftreestate () in
+  let pf = top_of_tree (proof_of_pftreestate pts) in
+    if is_leaf_proof pf then 
+      if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
+    else
+      errorlabstrm "Vernacentries.ExactProof" 
+	(str "Proof can only be used at the beginning of the proof")
 (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
  
    
-- 
cgit v1.2.3