Merge PR #9887: [api] Remove 8.10 deprecations.

Reviewed-by: SkySkimmer

14 files changed, 1 insertions, 169 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 96beb72a56..be0318fbde 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -26,24 +26,7 @@ let safe_evar_value sigma ev =
   try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
-(** Combinators *)
-
-let evd_comb0 f evdref =
-  let (evd',x) = f !evdref in
-    evdref := evd';
-    x
-
-let evd_comb1 f evdref x =
-  let (evd',y) = f !evdref x in
-    evdref := evd';
-    y
-
-let evd_comb2 f evdref x y =
-  let (evd',z) = f !evdref x y in
-    evdref := evd';
-    z
-
-let new_global evd x = 
+let new_global evd x =
   let (evd, c) = Evd.fresh_global (Global.env()) evd x in
   (evd, c)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index bb0da44103..8eaff8bd13 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-
 val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..d37b49e2dc 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -869,8 +869,6 @@ let to_universe_context evd = UState.context evd.universes
 
 let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
 
-let const_univ_entry = univ_entry
-
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
 let restrict_universe_context evd vars =
diff --git a/engine/evd.mli b/engine/evd.mli
index b0fcddb068..29235050b0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -615,9 +615,6 @@ val to_universe_context : evar_map -> Univ.UContext.t
 
 val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
 
-val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index ac0344148a..dab2e7d5ef 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
 
-let nf_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
-
 let enter f =
   bind goals
     (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 3c4fa6f4e8..ed95d62bc6 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** {5 Focussing} *)
 
-val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
-[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
-
 (** Enter a goal. The resulting tactic is focussed. *)
 
 val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..ecea637947 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1104,13 +1104,6 @@ module Goal = struct
         tclZERO ~info e
     end
     end
-
-  let normalize { self; state } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
   let gmake env sigma goal =
     let state = get_state goal in
     let goal = drop_state goal in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9455dae643..92f8b86df5 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -505,10 +505,6 @@ module Goal : sig
   (** Type of goals. *)
   type t
 
-  (** Normalises the argument goal. *)
-  val normalize : t -> t tactic
-  [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
-
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
diff --git a/engine/termops.ml b/engine/termops.ml
index 8e12c9be88..8a6bd17948 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
-let pr_sort_family = Sorts.pr_sort_family
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-let pr_fix = Constr.debug_print_fix
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
 let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
 let term_printer = ref debug_print_constr_env
@@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c =
   let c = Unsafe.to_constr (whd_evar sigma c) in
   Constr.fold_constr_with_binders g f n acc c
 
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
-   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let iter_constr_with_full_binders = EConstr.iter_with_full_binders
-
 (***************************)
 (* occurs check functions  *)
 (***************************)
@@ -862,8 +850,6 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference = vars_of_global
-
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
@@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l =
     | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
-let on_judgment = Environ.on_judgment
-let on_judgment_value = Environ.on_judgment_value
-let on_judgment_type = Environ.on_judgment_type
-
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
      variables skips let-in's; let-in's in the middle are put in ctx2 *)
 let context_chop k ctx =
diff --git a/engine/termops.mli b/engine/termops.mli
index 1dd9941c5e..a9217b3586 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -16,12 +16,6 @@ open Constr
 open Environ
 open EConstr
 
-(** printers *)
-val pr_sort_family : Sorts.family -> Pp.t
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 (** about contexts *)
 val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
 val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
@@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map ->
   ('a -> 'b -> constr -> 'b) ->
   'a -> 'b -> constr -> 'b
 
-val iter_constr_with_full_binders : Evd.evar_map ->
-  (rel_declaration -> 'a -> 'a) ->
-  ('a -> constr -> unit) -> 'a ->
-  constr -> unit
-[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
-
 (**********************************************************************)
 
 val strip_head_cast : Evd.evar_map -> constr -> constr
@@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
 
-val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
-
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
 val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
@@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool
 
 val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
-(** Combinators on judgments *)
-
-val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment]."]
-val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
-val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
-
 (** {5 Debug pretty-printers} *)
 
 open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index aa14f66df6..adea78d4c9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -116,8 +116,6 @@ let univ_entry ~poly uctx =
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
-let const_univ_entry = univ_entry
-
 let of_context_set ctx = { empty with uctx_local = ctx }
 
 let subst ctx = ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index a358813825..3df7f9e8e9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t
 val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
-val const_univ_entry : poly:bool -> t -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 (** {5 Constraints handling} *)
 
 val drop_weak_constraints : bool ref
diff --git a/engine/univGen.ml b/engine/univGen.ml
index c310331b15..f1deb1bfaf 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -25,11 +25,6 @@ let new_univ_global () =
 let fresh_level () =
   Univ.Level.make (new_univ_global ())
 
-(* TODO: remove *)
-let new_univ () = Univ.Universe.make (fresh_level ())
-let new_Type () = mkType (new_univ ())
-let new_Type_sort () = sort_of_univ (new_univ ())
-
 let fresh_instance auctx =
   let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
@@ -83,10 +78,6 @@ let constr_of_monomorphic_global gr =
       Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
           str " would forget universes.")
 
-let constr_of_global gr = constr_of_monomorphic_global gr
-
-let constr_of_global_univ = mkRef
-
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
   | IsGlobal gr -> fresh_global_instance env gr
@@ -99,34 +90,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-open Declarations
-
-let type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env, ContextSet.empty
-
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-     let ty = cb.const_type in
-     let auctx = Declareops.constant_polymorphic_context cb in
-     let inst, ctx = fresh_instance auctx in
-     Vars.subst_instance_constr inst ty, ctx
-
-  | IndRef ind ->
-    let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    let ty = Inductive.type_of_inductive env (specif, inst) in
-    ty, ctx
-
-  | ConstructRef (ind,_ as cstr) ->
-    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    Inductive.type_of_constructor (cstr,inst) specif, ctx
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
@@ -135,11 +98,6 @@ let fresh_sort_in_family = function
     let u = fresh_level () in
       sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
 
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family sf)
-
-let extend_context = Univ.extend_in_context_set
-
 let new_global_univ () =
   let u = fresh_level () in
   (Univ.Universe.make u, ContextSet.singleton u)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index b4598e10d0..34920e5620 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *)
 val new_univ_global : unit -> Level.UGlobal.t
 val fresh_level : unit -> Level.t
 
-val new_univ : unit -> Universe.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type : unit -> types
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type_sort : unit -> Sorts.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-
 val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
 
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
@@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> GlobRef.t puniverses
 
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-[@@ocaml.deprecated "Use [Constr.mkRef]"]
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t ->
-  'a in_universe_context_set
-[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
-
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an error on polymorphic constants/inductives:
     the constraints should be properly added to an evd.
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a polymorphic global reference. *)
 val constr_of_monomorphic_global : GlobRef.t -> constr
-
-val constr_of_global : GlobRef.t -> constr
-[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
-                     use [constr_of_monomorphic_global] if the reference is guaranteed to\
-                     be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
-    references and computing their instantiated universe context. (side-effect on the
-    universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
-[@@ocaml.deprecated "use [Typeops.type_of_global]"]