diff options
| -rw-r--r-- | kernel/typeops.ml | 24 | ||||
| -rw-r--r-- | kernel/typeops.mli | 10 | ||||
| -rw-r--r-- | library/global.ml | 21 |
3 files changed, 35 insertions, 20 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 164a47dd9a..c3a964d2db 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -319,6 +319,30 @@ let check_fixpoint env lna lar vdef vdeft = with NotConvertibleVect i -> error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar +(* Global references *) + +let type_of_global_in_context env r = + let open Names.GlobRef in + match r with + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + cb.Declarations.const_type, univs + | IndRef ind -> + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in + Inductive.type_of_inductive env (specif, inst), univs + | ConstructRef cstr -> + let (mib,_ as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs + (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 515e22c99b..e83c1b3dc5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -96,6 +96,16 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment +(** {6 Type of global references. } *) + +val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t +(** Returns the type of the global reference, by creating a fresh + instance of polymorphic references and computing their + instantiated universe context. The type should not be used + without pushing it's universe context in the environmnent of + usage. For non-universe-polymorphic constants, it does not + matter. *) + (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) diff --git a/library/global.ml b/library/global.ml index 1ad72afea1..1672d508c2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -189,26 +189,7 @@ let constr_of_global_in_context env r = let univs = Declareops.inductive_polymorphic_context mib in mkConstructU (cstr, Univ.make_abstract_instance univs), univs -let type_of_global_in_context env r = - match r with - | VarRef id -> Environ.named_type id env, Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - cb.Declarations.const_type, univs - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs +let type_of_global_in_context = Typeops.type_of_global_in_context let universes_of_global gr = universes_of_global (env ()) gr |