diff options
author | 2013-10-28 14:08:46 +0100 | |
---|---|---|
committer | 2014-05-06 09:58:54 +0200 | |
commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /library/universes.ml | |
parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'library/universes.ml')
-rw-r--r-- | library/universes.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/library/universes.ml b/library/universes.ml index c7009b400..73a0b2b1c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -144,17 +144,21 @@ let type_of_reference env r = | VarRef id -> Environ.named_type id env, ContextSet.empty | ConstRef c -> let cb = Environ.lookup_constant c env in + let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in - Vars.subst_univs_constr subst cb.const_type, ctx - else cb.const_type, ContextSet.empty + Vars.subst_univs_constr subst ty, ctx + else ty, ContextSet.empty | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in if mib.mind_polymorphic then let (inst, subst), ctx = fresh_instance_from mib.mind_universes in - Vars.subst_univs_constr subst oib.mind_arity.mind_user_arity, ctx - else oib.mind_arity.mind_user_arity, ContextSet.empty + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + else + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in if mib.mind_polymorphic then |