[api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.

4 files changed, 16 insertions, 99 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 978b1f6f78..778d98b2cd 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -126,9 +126,6 @@ type t =
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let initial_goals pf = Proofview.initial_goals pf.entry
-let initial_euctx pf = pf.initial_euctx
-
 (*** General proof functions ***)
 
 let proof p =
@@ -147,33 +144,6 @@ let proof p =
   let given_up = p.given_up in
   (goals,stack,shelf,given_up,sigma)
 
-type 'a pre_goals = {
-  fg_goals : 'a list;
-  (** List of the focussed goals *)
-  bg_goals : ('a list * 'a list) list;
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : 'a list;
-  (** List of the goals on the shelf. *)
-  given_up_goals : 'a list;
-  (** List of the goals that have been given up *)
-}
-
-let map_structured_proof pfts process_goal: 'a pre_goals =
-  let (goals, zipper, shelf, given_up, sigma) = proof pfts in
-  let fg = List.map (process_goal sigma) goals in
-  let map_zip (lg, rg) =
-    let lg = List.map (process_goal sigma) lg in
-    let rg = List.map (process_goal sigma) rg in
-    (lg, rg)
-  in
-  let bg = List.map map_zip zipper in
-  let shelf = List.map (process_goal sigma) shelf in
-  let given_up = List.map (process_goal sigma) given_up in
-    { fg_goals = fg;
-      bg_goals = bg;
-      shelved_goals = shelf;
-      given_up_goals = given_up; }
-
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
@@ -441,22 +411,6 @@ let in_proof p k = k (Proofview.return p.proofview)
 let unshelve p =
   { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
-let pr_proof p =
-  let p = map_structured_proof p (fun _sigma g -> g) in
-  Pp.(
-    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
-    let rec aux acc = function
-      | [] -> acc
-      | (before,after)::stack ->
-         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
-              pr_goal_list after) stack in
-    str "[" ++ str "focus structure: " ++
-               aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
-    str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
-    str "given up: " ++ pr_goal_list p.given_up_goals ++
-    str "]"
-  )
-
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
 
@@ -554,3 +508,19 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
   { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+
+let pr_proof p =
+  let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
+  Pp.(
+    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+    let rec aux acc = function
+      | [] -> acc
+      | (before,after)::stack ->
+         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+              pr_goal_list after) stack in
+    str "[" ++ str "focus structure: " ++
+               aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++
+    str "given up: " ++ pr_goal_list given_up ++
+    str "]"
+  )
diff --git a/proofs/proof.mli b/proofs/proof.mli
index defef57a8d..1f4748141a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -34,30 +34,6 @@
 (* Type of a proof. *)
 type t
 
-(* Returns a stylised view of a proof for use by, for instance,
-   ide-s. *)
-(* spiwack: the type of [proof] will change as we push more refined
-   functions to ide-s. This would be better than spawning a new nearly
-   identical function everytime. Hence the generic name. *)
-(* In this version: returns the focused goals, a representation of the
-   focus stack (the goals at each level), a representation of the
-   shelf (the list of goals on the shelf), a representation of the
-   given up goals (the list of the given up goals) and the underlying
-   evar_map *)
-val proof : t ->
-  Goal.goal list
-  * (Goal.goal list * Goal.goal list) list
-  * Goal.goal list
-  * Goal.goal list
-  * Evd.evar_map
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_goals : t -> (EConstr.constr * EConstr.types) list
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_euctx : t -> UState.t
-[@@ocaml.deprecated "use [Proof.data]"]
-
 type data =
   { sigma : Evd.evar_map
   (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
@@ -81,29 +57,6 @@ type data =
 
 val data : t -> data
 
-(* Generic records structured like the return type of proof *)
-type 'a pre_goals = {
-  fg_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the focussed goals *)
-  bg_goals : ('a list * 'a list) list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the goals on the shelf. *)
-  given_up_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the goals that have been given up *)
-}
-[@@ocaml.deprecated "use [Proof.data]"]
-
-(* needed in OCaml 4.05.0, not needed in newer ones *)
-[@@@ocaml.warning "-3"]
-val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"]
-[@@ocaml.deprecated "use [Proof.data]"]
-[@@@ocaml.warning "+3"]
-
 (*** General proof functions ***)
 val start
   :  name:Names.Id.t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7b3d9e534b..93031c2202 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -104,10 +104,6 @@ let db_pr_goal sigma g =
 let pr_gls gls =
   hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
-let pr_glls glls =
-  hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++
-         prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
-
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 218011c316..23e1e6f566 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -68,8 +68,6 @@ val pf_conv_x_leq  : Goal.goal sigma -> constr -> constr -> bool
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : Goal.goal sigma -> Pp.t
-val pr_glls   : Goal.goal list sigma -> Pp.t
-[@@ocaml.deprecated "Please move to \"new\" proof engine"]
 
 (** Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig