diff options
| author | aspiwack | 2011-04-29 15:03:25 +0000 |
|---|---|---|
| committer | aspiwack | 2011-04-29 15:03:25 +0000 |
| commit | d10841e20af67563b60d7cf91e251079b35b6636 (patch) | |
| tree | 5b3b2631b68b374eed85c93379ba081c790b4d3a /plugins | |
| parent | 1bfd55b3ffc5d6bb710f1155bcac43cb3a3a35d0 (diff) | |
Fixed a bug causing inconsistent states during proof editting.
Some toplevel commands (for instance the experimental bullets) are
composed of several atomic commands, the failure of one must imply
the failure of the whole toplevel command. This commit introduces
a system of transaction to that effect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index aa187cc749..5ac3e8e9ed 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -67,7 +67,7 @@ let vernac_decl_proof () = if Proof.is_done pf then Util.error "Nothing left to prove here." else - begin + Proof.transaction pf begin fun () -> Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -75,13 +75,17 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.return_from_tactic_mode () ; + Proof_global.set_proof_mode "Declarative" ; + Vernacentries.print_subgoals () + end let vernac_proof_instr instr = - Decl_proof_instr.proof_instr instr; - Vernacentries.print_subgoals () + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.proof_instr instr; + Vernacentries.print_subgoals () + end (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) |