From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Oct 2013 14:08:46 +0100 Subject: Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely). --- library/global.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'library/global.ml') 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 = -- cgit v1.2.3