diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f3c5da2ad2..cbdcc96aa9 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -100,13 +100,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) + Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) let unfocus () = - Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) let maximal_unfocus () = - Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) + Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e47776bd7d..6b5cb7492b 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -121,7 +121,7 @@ let start_proof_tac gls= tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by (Proofview.V82.tactic start_proof_tac); + ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac)); let p = Proof_global.give_me_the_proof () in Decl_mode.focus p @@ -1461,7 +1461,7 @@ let do_instr raw_instr pts = let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in - Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) + ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) else () end; postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with |