diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/class.ml | 6 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
5 files changed, 8 insertions, 6 deletions
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 = |