[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.

4 files changed, 0 insertions, 117 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 90d2b7abaf..e7f995c84e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -194,7 +194,6 @@ let tag_var = tag Tag.variable
     sl ++ id
 
   let pr_id = Id.print
-  let pr_name = Name.print
   let pr_qualid = pr_qualid
   let pr_patvar = pr_id
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index bca419c9ac..e7f71849a5 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -34,8 +34,6 @@ val pr_sep_com :
   constr_expr -> Pp.t
 
 val pr_id : Id.t -> Pp.t
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "alias of Names.Name.print"]
 
 val pr_qualid : qualid -> Pp.t
 val pr_patvar : Pattern.patvar -> Pp.t
diff --git a/printing/printer.ml b/printing/printer.ml
index 79654da6e7..990bdaad7d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,7 +17,6 @@ open Environ
 open Globnames
 open Nametab
 open Evd
-open Proof_type
 open Refiner
 open Constrextern
 open Ppconstr
@@ -98,20 +97,6 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
 let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
 let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c
 
-(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
-let pr_lconstr t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_lconstr_env env sigma t
-let pr_constr t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_constr_env env sigma t
-
-let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c)
-let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c)
-
-let pr_open_lconstr (_,c) = pr_leconstr c
-let pr_open_constr (_,c) = pr_econstr c
-
 let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
   (* Warning: clashes can occur with variables of same name in env but *)
   (* we also need to preserve the actual names of the patterns *)
@@ -122,13 +107,6 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
 let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
 
-let pr_constr_under_binders c =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_constr_under_binders_env env sigma c
-let pr_lconstr_under_binders c =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_lconstr_under_binders_env env sigma c
-
 let pr_etype_core goal_concl_style env sigma t =
   pr_constr_expr (extern_type goal_concl_style env sigma t)
 let pr_letype_core = Proof_diffs.pr_letype_core
@@ -136,13 +114,6 @@ let pr_letype_core = Proof_diffs.pr_letype_core
 let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
 let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
 
-let pr_ltype t =
-    let (sigma, env) = Pfedit.get_current_context () in
-    pr_ltype_env env sigma t
-let pr_type t =
-    let (sigma, env) = Pfedit.get_current_context () in
-    pr_type_env env sigma t
-
 let pr_etype_env env sigma c = pr_etype_core false env sigma c
 let pr_letype_env env sigma c = pr_letype_core false env sigma c
 let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
@@ -150,29 +121,15 @@ let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
 
-let pr_ljudge j =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_ljudge_env env sigma j
-
 let pr_lglob_constr_env env c =
   pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
 let pr_glob_constr_env env c =
   pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
 
-let pr_lglob_constr c =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_lglob_constr_env env c
-let pr_glob_constr c =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_glob_constr_env env c
-
 let pr_closed_glob_n_env env sigma n c =
   pr_constr_expr_n n (extern_closed_glob false env sigma c)
 let pr_closed_glob_env env sigma c =
   pr_constr_expr (extern_closed_glob false env sigma c)
-let pr_closed_glob c =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_closed_glob_env env sigma c
 
 let pr_lconstr_pattern_env env sigma c =
   pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
@@ -182,13 +139,6 @@ let pr_constr_pattern_env env sigma c =
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
 
-let pr_lconstr_pattern t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_lconstr_pattern_env env sigma t
-let pr_constr_pattern t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  pr_constr_pattern_env env sigma t
-
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
 let _ = Termops.Internal.set_print_constr
@@ -247,13 +197,6 @@ let safe_gen f env sigma c =
 
 let safe_pr_lconstr_env = safe_gen pr_lconstr_env
 let safe_pr_constr_env = safe_gen pr_constr_env
-let safe_pr_lconstr t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  safe_pr_lconstr_env env sigma t
-
-let safe_pr_constr t =
-  let (sigma, env) = Pfedit.get_current_context () in
-  safe_pr_constr_env env sigma t
 
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
@@ -889,19 +832,6 @@ let pr_goal_by_id ~proof id =
       pr_selected_subgoal (pr_id id) sigma g)
   with Not_found -> user_err Pp.(str "No such goal.")
 
-(* Elementary tactics *)
-
-let pr_prim_rule = function
-  | Refine c ->
-      (** FIXME *)
-      str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++
-      Constrextern.with_meta_as_hole pr_constr c
-
-(* Backwards compatibility *)
-
-let prterm = pr_lconstr
-
-
 (* Printer function for sets of Assumptions.assumptions.
    It is used primarily by the Print Assumptions command. *)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 96db7091a6..f9d1a62895 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -27,13 +27,9 @@ val enable_goal_names_printing     : bool ref
 (** Terms *)
 
 val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
-val pr_lconstr             : constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 val pr_constr_env          : env -> evar_map -> constr -> Pp.t
-val pr_constr              : constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
@@ -43,19 +39,11 @@ val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> co
     in case of remaining issues (such as reference not in env). *)
 
 val safe_pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
-val safe_pr_lconstr             : constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val safe_pr_constr_env          : env -> evar_map -> constr -> Pp.t
-val safe_pr_constr              : constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_econstr_env     : env -> evar_map -> EConstr.t -> Pp.t
-val pr_econstr         : EConstr.t -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
-val pr_leconstr         : EConstr.t -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_econstr_n_env    : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
 
@@ -63,54 +51,30 @@ val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
 val pr_open_constr_env     : env -> evar_map -> open_constr -> Pp.t
-val pr_open_constr         : open_constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_open_lconstr_env    : env -> evar_map -> open_constr -> Pp.t
-val pr_open_lconstr        : open_constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> Pp.t
-val pr_constr_under_binders      : constr_under_binders -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
-val pr_lconstr_under_binders     : constr_under_binders -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
 val pr_ltype_env           : env -> evar_map -> types -> Pp.t
-val pr_ltype               : types -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_type_env            : env -> evar_map -> types -> Pp.t
-val pr_type                : types -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_closed_glob_n_env   : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
-val pr_closed_glob         : closed_glob_constr -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
-val pr_ljudge              : EConstr.unsafe_judgment -> Pp.t * Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lglob_constr_env      : env -> 'a glob_constr_g -> Pp.t
-val pr_lglob_constr          : 'a glob_constr_g -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_glob_constr_env       : env -> 'a glob_constr_g -> Pp.t
-val pr_glob_constr           : 'a glob_constr_g -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
-val pr_lconstr_pattern     : constr_pattern -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> Pp.t
-val pr_constr_pattern      : constr_pattern -> Pp.t
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_cases_pattern       : cases_pattern -> Pp.t
 
@@ -222,16 +186,8 @@ val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
 
-val pr_prim_rule           : prim_rule -> Pp.t
-[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"]
-
 val print_and_diff : Proof.t option -> Proof.t option -> unit
 
-(** Backwards compatibility *)
-
-val prterm                 : constr -> Pp.t (** = pr_lconstr *)
-[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-
 (** Declarations for the "Print Assumption" command *)
 type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)