From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [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.
---
 proofs/proof.mli | 47 -----------------------------------------------
 1 file changed, 47 deletions(-)

(limited to 'proofs/proof.mli')

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
-- 
cgit v1.2.3