diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 14:49:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 71563ebb86a83bc7cdfc17f58493f59428d764b0 (patch) | |
| tree | 247d33d8021ede65e34ac6d2de3d4224f0c80e90 /library/global.ml | |
| parent | 1014de55656c2698500089d940a12f7e4b26a0de (diff) | |
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/library/global.ml b/library/global.ml index 3a74f535d..5fff26566 100644 --- a/library/global.ml +++ b/library/global.ml @@ -191,6 +191,25 @@ let type_of_global_unsafe r = 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 + | 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 type_of_global_in_context env r = match r with | VarRef id -> Environ.named_type id env, Univ.AUContext.empty |