Merge branch 'v8.5' into trunk

1 files changed, 5 insertions, 6 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc1372..07df7c7f09 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,25 +89,22 @@ let get_info sigma gl=
 let try_get_info sigma gl =
   Store.get (Goal.V82.extra sigma gl) info
 
-let get_stack pts =
+let get_goal_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
-  let inf = get_stack p in
+  let inf = get_goal_stack p in
   Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
 let unfocus () =
   Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus () = 
-  Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
 let get_top_stack pts =
   try
     Proof.get_at_focus proof_focus pts
@@ -116,6 +113,8 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
 let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"