[api] Remove deprecated objects in engine / interp / library

12 files changed, 0 insertions, 182 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index afedfe180..648f96035 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -875,6 +875,3 @@ let eq_constr_univs_test sigma1 sigma2 t u =
       (universes sigma2) fold t u sigma2
   in
   match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 3ab2d3e34..f271c14ea 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -259,12 +259,6 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo
 
 val meta_counter_summary_tag : int Summary.Dyn.tag
 
-(** Deprecated *)
-type type_constraint = types option
-[@@ocaml.deprecated "use the version in Evardefine"]
-type val_constraint = constr option
-[@@ocaml.deprecated "use the version in Evardefine"]
-
 val e_new_evar :
   env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 78d5d4c8f..0c9c3a29b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -132,8 +132,6 @@ end
 
 module Store = Store.Make ()
 
-type evar = Evar.t
-
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
 type evar_body =
@@ -1206,28 +1204,6 @@ module Monad =
 
 type unsolvability_explanation = SeveralInstancesFound of int
 
-(** Deprecated *)
-type evar_universe_context = UState.t
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let constrain_variables = UState.constrain_variables
-let evar_universe_context_of_binders = UState.of_binders
-let make_evar_universe_context e l =
-  let g = Environ.universes e in
-  match l with
-  | None -> UState.make g
-  | Some l -> UState.make_with_initial_binders g l
-let normalize_evar_universe_context_variables = UState.normalize_variables
-let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.minimize
-let nf_constraints = minimize_universes
-
 module MiniEConstr = struct
 
   module ESorts =
diff --git a/engine/evd.mli b/engine/evd.mli
index b2670ee51..c40e925d8 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -33,14 +33,6 @@ type etypes = econstr
 
 (** {5 Existential variables and unification states} *)
 
-type evar = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-(** Existential variables. *)
-
-(** {6 Evars} *)
-val string_of_existential : Evar.t -> string
-[@@ocaml.deprecated "use Evar.print"]
-
 (** {6 Evar filters} *)
 
 module Filter :
@@ -130,10 +122,6 @@ val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
 
 (** {6 Unification state} **)
 
-type evar_universe_context = UState.t
-[@@ocaml.deprecated "Alias of UState.t"]
-(** The universe context associated to an evar map *)
-
 type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
@@ -529,48 +517,11 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * UState.t
 
-val evar_universe_context_set : UState.t -> Univ.ContextSet.t
-[@@ocaml.deprecated "Alias of UState.context_set"]
-val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
-[@@ocaml.deprecated "Alias of UState.constraints"]
-val evar_context_universe_context : UState.t -> Univ.UContext.t
-[@@ocaml.deprecated "alias of UState.context"]
-
-val evar_universe_context_of : Univ.ContextSet.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_context_set"]
-val empty_evar_universe_context : UState.t
-[@@ocaml.deprecated "Alias of UState.empty"]
-val union_evar_universe_context : UState.t -> UState.t ->
-  UState.t
-[@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst
-[@@ocaml.deprecated "Alias of UState.subst"]
-val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.constrain_variables"]
-
-
-val evar_universe_context_of_binders :
-  UnivNames.universe_binders -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_binders"]
-
-val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
-[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
 val universe_binders : evar_map -> UnivNames.universe_binders
-val add_constraints_context : UState.t ->
-  Univ.Constraint.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.add_constraints"]
-
-
-val normalize_evar_universe_context_variables : UState.t -> 
-  Univ.universe_subst in_evar_universe_context
-[@@ocaml.deprecated "Alias of UState.normalize_variables"]
-
-val normalize_evar_universe_context : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.minimize"]
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
 val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -627,8 +578,6 @@ val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
-val abstract_undefined_variables : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
 
 val fix_undefined_variables : evar_map -> evar_map
 
@@ -636,8 +585,6 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 (** Universe minimization *)
 val minimize_universes : evar_map -> evar_map
-val nf_constraints : evar_map -> evar_map
-[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
 
 val update_sigma_env : evar_map -> env -> evar_map
 
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 53969cafa..735a59fe5 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -11,10 +11,6 @@
 open Util
 open Names
 
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -191,28 +187,6 @@ struct
 
 end
 
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-let pr_name = print
-
-let pr_lab l = Label.print l
-
 (* Metavariables *)
 let pr_meta = Pp.int
 let string_of_meta = string_of_int
-
-(* Deprecated *)
-open Libnames
-let default_library = default_library
-let coq_string = coq_string
-let coq_root = coq_root
-let default_root_prefix = default_root_prefix
-
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 96842dfb9..8a93fad8c 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -94,47 +94,3 @@ end
 (** Metavariables *)
 val pr_meta : Constr.metavariable -> Pp.t
 val string_of_meta : Constr.metavariable -> string
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** Deprecated stuff to libnames *)
-val default_library : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-
-val coq_root : module_ident (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
-
-val coq_string : string (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-
-val default_root_prefix : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 54237ceb4..fdb0a215d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1085,8 +1085,6 @@ module Goal = struct
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  let assume (gl : t) = (gl : t)
-
   let print { sigma; self } = { Evd.it = self; sigma }
 
   let state { state=state } = state
@@ -1274,11 +1272,6 @@ module V82 = struct
       
     
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  let goals { comb = comb ; solution = solution; } =
-   { Evd.it = List.map drop_state comb ; sigma = solution }
-
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 1905686fe..970bf6773 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -495,10 +495,6 @@ module Goal : sig
   (** Type of goals. *)
   type t
 
-  (** Assume that you do not need the goal to be normalized. *)
-  val assume : t -> t
-  [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"]
-
   (** Normalises the argument goal. *)
   val normalize : t -> t tactic
 
@@ -589,11 +585,6 @@ module V82 : sig
      (in chronological order of insertion). *)
   val grab : proofview -> proofview
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interpret them. *)
-  val goals : proofview -> Evar.t list Evd.sigma
-  [@@ocaml.deprecated "Use [Proofview.proofview]"]
-
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
 
   (* returns the existential variable used to start the proof *)
diff --git a/engine/termops.ml b/engine/termops.ml
index c52f96079..51fc59289 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -974,9 +974,6 @@ let count_occurrences sigma m t =
   countrec m t;
   !n
 
-(* Synonymous *)
-let occur_term = dependent
-
 let pop t = EConstr.Vars.lift (-1) t
 
 (***************************)
diff --git a/engine/termops.mli b/engine/termops.mli
index e2ddcd36e..bb3cbb6a8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -113,8 +113,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
-val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
-[@@ocaml.deprecated "alias of Termops.dependent"]
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 844eb390b..15cf4d4c1 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -663,6 +663,3 @@ let update_sigma_env uctx env =
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
   prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
-
-(** Deprecated *)
-let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 11aaaf389..d1678a155 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -137,8 +137,6 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 (** Universe minimization *)
 val minimize : t -> t
-val normalize : t -> t
-[@@ocaml.deprecated "Alias of UState.minimize"]
 
 type universe_decl =
   (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl