Remove the function Global.type_of_global_unsafe.

15 files changed, 25 insertions, 50 deletions

diff --git a/API/API.mli b/API/API.mli
index f8fb96aa9..e8418552c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2713,7 +2713,6 @@ sig
 
   val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
   val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
-  val type_of_global_unsafe : Globnames.global_reference -> Term.types
 
   val current_dirpath : unit -> Names.DirPath.t
   val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
diff --git a/interp/notation.ml b/interp/notation.ml
index 4067a6b94..c07a00943 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -718,13 +718,13 @@ let rebuild_arguments_scope (req,r,n,l,_) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-        let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in
+        let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in
 	(req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
            for the extra parameters of the section. Discard the classes
            of the manually given scopes to avoid further re-computations. *)
-        let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
+        let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in
 	let l1 = List.firstn n l' in
         let cls1 = List.firstn n cls in
 	(req,r,0,l1@l,cls1)
@@ -768,7 +768,7 @@ let find_arguments_scope r =
   with Not_found -> []
 
 let declare_ref_arguments_scope ref =
-  let t = Global.type_of_global_unsafe ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let (scs,cls as o) = compute_arguments_scope_full t in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
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
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2642aeefa..dff3548fd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -445,9 +445,10 @@ let error_MPfile_as_mod mp b =
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let argnames_of_global r =
-  let typ = Global.type_of_global_unsafe r in
+  let env = Global.env () in
+  let typ, _ = Global.type_of_global_in_context env r in
   let rels,_ =
-    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+    decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -878,7 +879,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Global.type_of_global_unsafe (ConstRef kn) in
+	let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3..61fbca23f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -342,7 +342,7 @@ let pr_info f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr
-       (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+       (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c4418b5a6..d4fa266c0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -400,7 +400,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty = Global.type_of_global_unsafe glob in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 5cd79ed6d..827c0e458 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -70,7 +70,8 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref =
-  let typ = Global.type_of_global_unsafe ref in
+  let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
+  let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
@@ -137,7 +138,7 @@ let print_renames_list prefix l =
     hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
 
 let need_expansion impl ref =
-  let typ = Global.type_of_global_unsafe ref in
+  let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let ctx = prod_assum typ in
   let nprods = List.count is_local_assum ctx in
   not (List.is_empty impl) && List.length impl >= nprods &&
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c2c80e630..a572508d4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -937,7 +937,7 @@ let make_extern pri pat tacast =
 
 let make_mode ref m = 
   let open Term in
-  let ty = Global.type_of_global_unsafe ref in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
   let m' = Array.of_list m in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 248224e6b..59920742d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -105,7 +105,7 @@ let mkFullInd (ind,u) n =
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
-  try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
+  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
diff --git a/vernac/class.ml b/vernac/class.ml
index 0b510bbcf..be682977e 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -62,7 +62,9 @@ let explain_coercion_error g = function
 (* Verifications pour l'ajout d'une classe *)
 
 let check_reference_arity ref =
-  if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
+  let env = Global.env () in
+  let c, _ = Global.type_of_global_in_context env ref in
+  if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
@@ -252,7 +254,7 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t = Global.type_of_global_unsafe coef in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
   let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6d4b164b..ab1892a18 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -68,7 +68,7 @@ let _ =
 let existing_instance glob g info =
   let c = global g in
   let info = Option.default Hints.empty_hint_info info in
-  let instance = Global.type_of_global_unsafe c in
+  let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
diff --git a/vernac/search.ml b/vernac/search.ml
index 5cf6a9491..0f56f81e7 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -78,7 +78,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
     let gr = ConstRef cst in
-    let typ = Global.type_of_global_unsafe gr in
+    let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
   | "INDUCTIVE" ->
     let mind = Global.mind_of_delta_kn kn in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bbec28aff..8a647c6c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -986,7 +986,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
 
   let sr = smart_global reference in
   let inf_names =
-    let ty = Global.type_of_global_unsafe sr in
+    let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
     Impargs.compute_implicits_names (Global.env ()) ty
   in
   let prev_names =