diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 23 |
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 *) |