From 8cada511701d8893bab5553470ab721b33713043 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 02:55:51 +0100
Subject: [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.
---
 proofs/pfedit.ml | 5 ++---
 proofs/proof.ml  | 7 +++++--
 proofs/proof.mli | 2 +-
 3 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2d4aba17cb..c526ae000a 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 e24d57f088..413b5fdd7e 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 48aed8225e..5756d06b64 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
-- 
cgit v1.2.3