diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c3a964d2db..3481d3bedb 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -343,6 +343,28 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs +(* Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +let constr_of_global_in_context env r = + let open GlobRef in + match r with + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + mkConstU (c, Univ.make_abstract_instance univs), univs + | IndRef ind -> + let (mib,_) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + mkIndU (ind, Univ.make_abstract_instance univs), univs + | ConstructRef cstr -> + let (mib,_) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + mkConstructU (cstr, Univ.make_abstract_instance univs), univs + (************************************************************************) (************************************************************************) |