3 files changed, 8 insertions, 6 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2d4aba17c..c526ae000 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,9 +51,8 @@ end
 
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
-  let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
-  try
-          { it=(List.nth goals (i-1)) ; sigma=sigma; }
+  let goals,_,_,_,sigma = Proof.proof p in
+  try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
 let get_goal_context_gen i =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e24d57f08..413b5fdd7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -163,6 +163,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals =
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
+
 (* spiwack: a proof is considered completed even if its still focused, if the focus
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
@@ -391,10 +392,12 @@ let pr_proof p =
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
-    Proofview.V82.goals p.proofview
+    let it, sigma = Proofview.proofview p.proofview in
+    Evd.{ it; sigma }
 
   let background_subgoals p =
-    Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
+    let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
+    Evd.{ it; sigma }
 
   let top_goal p =
     let { Evd.it=gls ; sigma=sigma; } =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 48aed8225..5756d06b6 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -65,7 +65,6 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 
 
 (*** General proof functions ***)
-
 val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (EConstr.constr * EConstr.types) list
@@ -187,6 +186,7 @@ val pr_proof : proof -> Pp.t
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
   val subgoals : proof -> Goal.goal list Evd.sigma
+  [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
 
   (* All the subgoals of the proof, including those which are not focused. *)
   val background_subgoals : proof -> Goal.goal list Evd.sigma