diff options
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. *) |