diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/global.ml | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/library/declare.ml b/library/declare.ml index 06eeeeab5..f3150174c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; - mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty); + mind_entry_universes = Univ.UInfoInd.empty; mind_entry_private = None; }) diff --git a/library/global.ml b/library/global.ml index 1ba86699d..a45998384 100644 --- a/library/global.ml +++ b/library/global.ml @@ -178,13 +178,13 @@ let type_of_global_unsafe r = 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 + Univ.UContext.instance (Univ.UInfoInd.univ_context 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 + let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in Inductive.type_of_constructor (cstr,inst) specif let type_of_global_in_context env r = @@ -200,13 +200,13 @@ let type_of_global_in_context env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty 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 = - if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.UContext.empty in let inst = Univ.UContext.instance univs in @@ -222,10 +222,10 @@ let universes_of_global env r = (Environ.opaque_tables env) cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) | ConstructRef cstr -> let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Univ.instantiate_univ_context mib.mind_universes + Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) let universes_of_global gr = universes_of_global (env ()) gr |