[proof] Attempt to deprecate some V82 parts of the proof API.

I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.

However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.

Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.

11 files changed, 29 insertions, 21 deletions

diff --git a/API/API.mli b/API/API.mli
index 704f1a356..fd5f3cf09 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4645,16 +4645,23 @@ sig
   type proof
   type 'a focus_kind
 
+  val proof : proof ->
+    Goal.goal list * (Goal.goal list * Goal.goal list) list *
+    Goal.goal list * Goal.goal list * Evd.evar_map
+
   val run_tactic : Environ.env ->
                    unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree)
   val unshelve : proof -> proof
   val maximal_unfocus : 'a focus_kind -> proof -> proof
   val pr_proof : proof -> Pp.t
+
   module V82 :
   sig
     val grab_evars : proof -> proof
 
     val subgoals : proof -> Goal.goal list Evd.sigma
+    [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
+
   end
 end
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0379d4b49..7f7acf874 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -563,6 +563,7 @@ module V82 : sig
   (* Returns the open goals of the proofview together with the evar_map to 
      interpret them. *)
   val goals : proofview -> Evar.t list Evd.sigma
+  [@@ocaml.deprecated "Use [Proofview.proofview]"]
 
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
   
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 7cbab56d4..cfc0e09a0 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -217,7 +217,7 @@ let evars () =
     let doc = get_doc () in
     set_doc @@ Stm.finish ~doc;
     let pfts = Proof_global.give_me_the_proof () in
-    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+    let all_goals, _, _, _, sigma = Proof.proof pfts in
     let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
     let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
     let el = List.map map_evar exl in
@@ -227,7 +227,7 @@ let evars () =
 let hints () =
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+    let all_goals, _, _, _, sigma = Proof.proof pfts in
     match all_goals with
     | [] -> None
     | g :: _ ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2fdc3bc37..b8d41d539 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1225,8 +1225,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 
 let get_current_subgoals_types () =
   let p = Proof_global.give_me_the_proof () in
-  let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
-    sigma, List.map (Goal.V82.abstract_type sigma) sgs
+  let sgs,_,_,_,sigma = Proof.proof p in
+  sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
 exception EmptySubgoals
 let build_and_l sigma l =
diff --git a/printing/printer.ml b/printing/printer.ml
index 075b03b7d..ba31b72d6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -828,7 +828,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 
 let pr_nth_open_subgoal n =
   let pf = Proof_global.give_me_the_proof () in
-  let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+  let gls,_,_,_,sigma = Proof.proof pf in
   pr_subgoal n sigma gls
 
 let pr_goal_by_id id =
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
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c7c53b393..99be1846c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1467,11 +1467,11 @@ let pr_hint_term sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint () =
   let pts = Proof_global.give_me_the_proof () in
-  let glss = Proof.V82.subgoals pts in
-  match glss.Evd.it with
+  let glss,_,_,_,sigma = Proof.proof pts in
+  match glss with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
-    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
+    pr_hint_term sigma (Goal.V82.concl sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cc9d98f6f..62f3866de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       invEnv ~init:Context.Named.empty
   end in
   let avoid = ref Id.Set.empty in
-  let { sigma=sigma } = Proof.V82.subgoals pf in
+  let _,_,_,_,sigma = Proof.proof pf in
   let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
     match EConstr.kind sigma c with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5bcb3b1e1..8501813e9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -62,14 +62,12 @@ let show_proof () =
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = Proof_global.give_me_the_proof () in
-  let gls = Proof.V82.subgoals pfts in
-  let sigma = gls.Evd.sigma in
+  let gls,_,_,_,sigma = Proof.proof pfts in
   Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma))
 
 let show_universes () =
   let pfts = Proof_global.give_me_the_proof () in
-  let gls = Proof.V82.subgoals pfts in
-  let sigma = gls.Evd.sigma in
+  let gls,_,_,_,sigma = Proof.proof pfts in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
     Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
@@ -78,7 +76,7 @@ let show_universes () =
 let show_intro all =
   let open EConstr in
   let pf = Proof_global.give_me_the_proof() in
-  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gls,_,_,_,sigma = Proof.proof pf in
   if not (List.is_empty gls) then begin
     let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
     let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
@@ -1601,7 +1599,7 @@ let vernac_global_check c =
 
 let get_nth_goal n =
   let pf = Proof_global.give_me_the_proof() in
-  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gls,_,_,_,sigma = Proof.proof pf in
   let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
   gl