Remove the function Global.type_of_global_unsafe.

3 files changed, 4 insertions, 32 deletions

diff --git a/library/global.ml b/library/global.ml
index 5fff26566..5b17855dc 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -173,24 +173,6 @@ open Globnames
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
-let type_of_global_unsafe r = 
-  let env = env() in
-  match r with
-  | VarRef id -> Environ.named_type id env
-  | ConstRef c -> 
-    let cb = Environ.lookup_constant c env in 
-    let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in
-    let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
-    Vars.subst_instance_constr inst ty
-  | IndRef ind ->
-    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
-    Inductive.type_of_inductive env (specif, inst)
-  | ConstructRef cstr ->
-    let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
-    Inductive.type_of_constructor (cstr,inst) specif
-
 let constr_of_global_in_context env r =
   let open Constr in
   match r with
diff --git a/library/global.mli b/library/global.mli
index 0f1cec44a..431747c52 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -136,17 +136,6 @@ val type_of_global_in_context : Environ.env ->
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
-val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
-(** Returns the type of the constant, forgetting its universe context if
-    it is polymorphic, use with care: for polymorphic constants, the
-    type cannot be used to produce a term used by the kernel.  For safe
-    handling of polymorphic global references, one should look at a
-    particular instantiation of the reference, in some particular
-    universe context (part of an [env] or [evar_map]), see
-    e.g. [type_of_constant_in]. If you want to create a fresh instance
-    of the reference and get its type look at [Evd.fresh_global] or
-    [Evarutil.new_global] and [Retyping.get_type_of]. *)
-
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 351addf2f..b7125fc85 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -431,12 +431,13 @@ let compute_mib_implicits flags manual kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
 	  (** No need to care about constraints here *)
-	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i))))
+	  let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar = Global.type_of_global_unsafe (IndRef ind) in
+    let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
     ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
      Array.mapi (fun j c ->
        (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
@@ -674,7 +675,7 @@ let projection_implicits env p impls =
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
-  let t = Global.type_of_global_unsafe ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let enriching = Option.default flags.auto enriching in
   let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
   let l' = match l with