[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.

1 files changed, 7 insertions, 0 deletions

diff --git a/API/API.mli b/API/API.mli
index 704f1a3569..fd5f3cf092 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