Remove the function Global.type_of_global_unsafe.

5 files changed, 8 insertions, 6 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 248224e6b7..59920742d8 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 0b510bbcf0..be682977e5 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 d6d4b164b3..ab1892a18e 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 5cf6a94912..0f56f81e74 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 bbec28afff..8a647c6c18 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 =