From 5944946b01c436a167a7b86b22084d12114b59df Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 16 Jan 2006 10:38:07 +0000
Subject: Correction dans vernac_exact_proof -- jmn

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 499190a839..ac4a5c33a2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -345,8 +345,8 @@ let vernac_end_proof = function
      the theories [??] *)
 
 let vernac_exact_proof c =
-  let pts = get_pftreestate () in
-  let pf = top_of_tree (proof_of_pftreestate pts) in
+  let pts = top_of_tree (get_pftreestate ()) in
+  let pf = (proof_of_pftreestate pts) in
     if is_leaf_proof pf then 
       begin by (Tactics.exact_proof c); save_named true end
     else
@@ -568,8 +568,8 @@ 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";
-  let pts = get_pftreestate () in
-  let pf = top_of_tree (proof_of_pftreestate pts) in
+  let pts = top_of_tree (get_pftreestate ()) in
+  let pf = (proof_of_pftreestate pts) in
     if is_leaf_proof pf then 
       if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
     else
-- 
cgit v1.2.3