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