diff options
| author | coq | 2006-01-16 10:38:07 +0000 |
|---|---|---|
| committer | coq | 2006-01-16 10:38:07 +0000 |
| commit | 5944946b01c436a167a7b86b22084d12114b59df (patch) | |
| tree | 48577087bb04a86c3de756623336ce33bdd05ba0 | |
| parent | 44510966ab7240c60f28f4f2e99d382e155b084b (diff) | |
Correction dans vernac_exact_proof -- jmn
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7876 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files 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 |