diff options
| -rw-r--r-- | kernel/typeops.ml | 22 | ||||
| -rw-r--r-- | kernel/typeops.mli | 8 | ||||
| -rw-r--r-- | library/global.ml | 23 |
3 files changed, 31 insertions, 22 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 + (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e83c1b3dc5..1fd070d9d5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -106,6 +106,14 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t usage. For non-universe-polymorphic constants, it does not matter. *) +(** {6 Building a term from a global reference *) + +(** Map a global reference to a term in its local universe + context. The term should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) +val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t + (** {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 1672d508c2..3781ff3230 100644 --- a/library/global.ml +++ b/library/global.ml @@ -167,28 +167,7 @@ let env_of_context hyps = open Globnames -(** 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 Constr in - match r with - | VarRef id -> mkVar id, Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.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, oib as specif) = 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,oib as specif) = - 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 - +let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context let universes_of_global gr = |