diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 24 |
1 files changed, 24 insertions, 0 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 + (************************************************************************) (************************************************************************) |