[api] Remove (most) 8.9 deprecated objects.

A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.

8 files changed, 0 insertions, 60 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e978adf761..bae13dbba1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1386,8 +1386,6 @@ let solve_unif_constraints_with_heuristics env
   check_problems_are_solved env heuristic_solved_evd;
   solve_unconstrained_impossible_cases env heuristic_solved_evd
 
-let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
-
 (* Main entry points *)
 
 exception UnableToUnify of evar_map * unification_error
@@ -1414,13 +1412,3 @@ let conv env ?(ts=default_transparent_state env) evd t1 t2 =
 
 let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
   make_opt(evar_conv_x ts env evd CUMUL t1 t2)
-
-let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
-  match evar_conv_x ts env !evdref CONV t1 t2 with
-  | Success evd' -> evdref := evd'; true
-  | _ -> false
-
-let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 =
-  match evar_conv_x ts env !evdref CUMUL t1 t2 with
-  | Success evd' -> evdref := evd'; true
-  | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index cdf5dd0e50..20a4f34ec7 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -27,12 +27,6 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
 
 (** The same function resolving evars by side-effect and
    catching the exception *)
-val e_conv  : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
-[@@ocaml.deprecated "Use [Evarconv.conv]"]
-
-val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
-[@@ocaml.deprecated "Use [Evarconv.cumul]"]
-
 val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
 val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
 
@@ -43,9 +37,6 @@ val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar
 
 val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
 
-val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
-[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"]
-
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 2dd3721980..c0565f4f47 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1690,8 +1690,6 @@ let reconsider_unif_constraints conv_algo evd =
     (Success evd)
     pbs
 
-let reconsider_conv_pbs = reconsider_unif_constraints
-
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3f05c58c41..4665ed29a2 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -62,9 +62,6 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
 
 val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
 
-val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
-[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"]
-
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 0fa573b9a6..ea222397a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,10 +269,6 @@ let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_kelim
 
-let projection_nparams_env _ p = Projection.npars p
-
-let projection_nparams p = Projection.npars p
-
 let has_dependent_elim mib =
   match mib.mind_record with
   | PrimRecord _ -> mib.mind_finite == BiFinite
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ea34707bfc..b2e205115f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,15 +129,9 @@ val allowed_sorts : env -> inductive -> Sorts.family list
 val has_dependent_elim : mutual_inductive_body -> bool
 
 (** Primitive projections *)
-val projection_nparams : Projection.t -> int
-[@@ocaml.deprecated "Use [Projection.npars]"]
-val projection_nparams_env : env -> Projection.t -> int
-[@@ocaml.deprecated "Use [Projection.npars]"]
-
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 				     EConstr.t -> EConstr.types -> types
 
-
 (** Extract information from an inductive family *)
 
 type constructor_summary = {
@@ -152,8 +146,6 @@ val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
 val get_constructors : env -> inductive_family -> constructor_summary array
-val get_projections  : env -> inductive -> Projection.Repr.t array option
-[@@ocaml.deprecated "Use [Environ.get_projections]"]
 
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4ba715f0d5..dc3f042431 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -398,9 +398,6 @@ let check env sigma c t =
     error_actual_type_core env sigma j t
   | Some sigma -> sigma
 
-let e_check env evdref c t =
-  evdref := check env !evdref c t
-
 (* Type of a constr *)
 
 let unsafe_type_of env sigma c =
@@ -416,9 +413,6 @@ let sort_of env sigma c =
   let sigma, a = type_judgment env sigma j in
   sigma, a.utj_type
 
-let e_sort_of env evdref c =
-  Evarutil.evd_comb1 (sort_of env) evdref c
-
 (* Try to solve the existential variables by typing *)
 
 let type_of ?(refresh=false) env sigma c =
@@ -429,16 +423,10 @@ let type_of ?(refresh=false) env sigma c =
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type
     else sigma, j.uj_type
 
-let e_type_of ?refresh env evdref c =
-  Evarutil.evd_comb1 (type_of ?refresh env) evdref c
-
 let solve_evars env sigma c =
   let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
   sigma, nf_evar sigma j.uj_val
 
-let e_solve_evars env evdref c =
-  Evarutil.evd_comb1 (solve_evars env) evdref c
-
 let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 3cf43ace01..b8830ff4a2 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -24,27 +24,17 @@ val unsafe_type_of : env -> evar_map -> constr -> types
     universes *)
 val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
-(** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
-[@@ocaml.deprecated "Use [Typing.type_of]"]
-
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
-val e_sort_of : env -> evar_map ref -> types -> Sorts.t
-[@@ocaml.deprecated "Use [Typing.sort_of]"]
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val check : env -> evar_map -> constr -> types -> evar_map
-val e_check   : env -> evar_map ref -> constr -> types -> unit
-[@@ocaml.deprecated "Use [Typing.check]"]
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> evar_map * constr
-val e_solve_evars : env -> evar_map ref -> constr -> constr
-[@@ocaml.deprecated "Use [Typing.solve_evars]"]
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)