diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..152ccb0798 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') = else Univ.Instance.empty | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..074b7373c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes) else 0 in let mk u = |