diff options
Diffstat (limited to 'plugins/decl_mode/decl_mode.ml')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 8c5aec38b..0cbd26316 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -99,11 +99,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof.focus proof_cond inf 1 p + Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) -let unfocus = Proof.unfocus proof_focus +let unfocus () = + Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus = Proof_global.maximal_unfocus proof_focus +let maximal_unfocus () = + Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try |