diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /library/global.ml | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/library/global.ml b/library/global.ml index 16b07db25..fbba81b51 100644 --- a/library/global.ml +++ b/library/global.ml @@ -151,10 +151,16 @@ let type_of_global_unsafe r = match r with | VarRef id -> Environ.named_type id env | ConstRef c -> - let cb = Environ.lookup_constant c env in cb.Declarations.const_type + let cb = Environ.lookup_constant c env in + Typeops.type_of_constant_type env cb.Declarations.const_type | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in - oib.Declarations.mind_arity.Declarations.mind_user_arity + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let inst = + if mib.Declarations.mind_polymorphic then + Univ.UContext.instance mib.Declarations.mind_universes + else Univ.Instance.empty + in + Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let inst = Univ.UContext.instance mib.Declarations.mind_universes in @@ -169,13 +175,13 @@ let type_of_global_in_context env r = let univs = if cb.const_polymorphic then Future.force cb.const_universes else Univ.UContext.empty - in cb.Declarations.const_type, univs + in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = if mib.mind_polymorphic then mib.mind_universes else Univ.UContext.empty - in oib.Declarations.mind_arity.Declarations.mind_user_arity, univs + in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = |