- correction du bug #1055

- modification des propriétés sur trunk et trunk/test-suite



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8665 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 77075e2fa7..ad725bb5cf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -344,8 +344,14 @@ let vernac_end_proof = function
      the theories [??] *)
 
 let vernac_exact_proof c =
-  by (Tactics.exact_proof c);
-  save_named true
+  let pfs = top_of_tree (get_pftreestate()) in
+  let pf = proof_of_pftreestate pfs in
+    if (is_leaf_proof pf) then begin
+      by (Tactics.exact_proof c);
+      save_named true end
+    else
+      errorlabstrm "Vernacentries.ExactProof"
+	(str "Command '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
@@ -562,10 +568,15 @@ 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)
-    (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
- 
-   
+  let pfs = top_of_tree (get_pftreestate()) in
+  let pf = proof_of_pftreestate pfs in
+    if (is_leaf_proof pf) then
+      if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
+	(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+    else
+      errorlabstrm "Vernacentries.ExactProof"
+	(str "Command 'Proof ...' can only be used at the beginning of the proof")
+	
 (*****************************)
 (* Auxiliary file management *)