From 469a9b3242891b089b4a211e96b5b568277f7fc0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 15:55:51 +0200 Subject: Remove the function Global.type_of_global_unsafe. --- API/API.mli | 1 - interp/notation.ml | 6 +++--- library/global.ml | 18 ------------------ library/global.mli | 11 ----------- library/impargs.ml | 7 ++++--- plugins/extraction/table.ml | 7 ++++--- plugins/funind/indfun_common.ml | 2 +- pretyping/typeclasses.ml | 2 +- printing/prettyp.ml | 5 +++-- tactics/hints.ml | 2 +- vernac/auto_ind_decl.ml | 2 +- vernac/class.ml | 6 ++++-- vernac/classes.ml | 2 +- vernac/search.ml | 2 +- vernac/vernacentries.ml | 2 +- 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 = -- cgit v1.2.3