aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.ml18
-rw-r--r--library/global.mli11
-rw-r--r--library/impargs.ml7
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