diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-30 18:48:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-30 18:53:32 +0200 |
| commit | 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 (patch) | |
| tree | 3e5b4098318c4bbad4024d072c5008825e78c1c9 /library/global.ml | |
| parent | dac4d8952c5fc234f5b6245e39a73c2ca07555ee (diff) | |
Simplify even further the declaration of primitive projections,
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 65e895dfd..adfb7cafe 100644 --- a/library/global.ml +++ b/library/global.ml @@ -152,7 +152,9 @@ let type_of_global_unsafe r = | VarRef id -> Environ.named_type id env | ConstRef c -> let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env cb.Declarations.const_type + let univs = Declareops.universes_of_polymorphic_constant cb in + let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in + Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let inst = @@ -195,7 +197,7 @@ let universes_of_global env r = | VarRef id -> Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_constant cb + Declareops.universes_of_polymorphic_constant cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Univ.instantiate_univ_context mib.mind_universes |