Merge PR #9952: Remove `constr_of_global_in_context`

Reviewed-by: ppedrot

4 files changed, 0 insertions, 35 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 12ffbf4357..af710e7822 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -462,28 +462,6 @@ let type_of_global_in_context env r =
     let inst = Univ.make_abstract_instance univs in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
-(* Build a fresh instance for a given context, its associated substitution and
-   the instantiated constraints. *)
-
-let constr_of_global_in_context env r =
-  let open GlobRef in
-  match r with
-  | VarRef id -> mkVar id, Univ.AUContext.empty
-  | ConstRef c ->
-    let cb = lookup_constant c env in
-    let univs = Declareops.constant_polymorphic_context cb in
-    mkConstU (c, Univ.make_abstract_instance univs), univs
-  | IndRef ind ->
-    let (mib,_) = Inductive.lookup_mind_specif env ind in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkIndU (ind, Univ.make_abstract_instance univs), univs
-  | ConstructRef cstr ->
-    let (mib,_) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
-    in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
-
 (************************************************************************)
 (************************************************************************)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cc1885f42d..c8f3e506e6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -107,14 +107,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
     usage. For non-universe-polymorphic constants, it does not
     matter. *)
 
-(** {6 Building a term from a global reference *)
-
-(** Map a global reference to a term in its local universe
-    context. The term should not be used without pushing it's universe
-    context in the environmnent of usage. For non-universe-polymorphic
-    constants, it does not matter. *)
-val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
-
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
diff --git a/library/global.ml b/library/global.ml
index d9f8a6ffa3..55aed1c56e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -157,7 +157,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-let constr_of_global_in_context = Typeops.constr_of_global_in_context
 let type_of_global_in_context = Typeops.type_of_global_in_context
 
 let universes_of_global gr = 
diff --git a/library/global.mli b/library/global.mli
index ca88d2dafd..76ac3f6279 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -131,10 +131,6 @@ val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
 val is_type_in_type : GlobRef.t -> bool
 
-val constr_of_global_in_context : Environ.env ->
-  GlobRef.t -> Constr.types * Univ.AUContext.t
-  [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"]
-
 val type_of_global_in_context : Environ.env -> 
   GlobRef.t -> Constr.types * Univ.AUContext.t
   [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]