diff options
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 2d04b77e4..8c10bd6ec 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -97,8 +97,8 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let u = check bool_equal (fun x -> x.mind_polymorphic); if mib1.mind_polymorphic then ( - check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes); - Univ.UContext.instance mib1.mind_universes) + check Univ.Instance.equal (fun x -> Univ.UContext.instance (Univ.UInfoInd.univ_context x.mind_universes)); + Univ.UContext.instance (Univ.UInfoInd.univ_context mib1.mind_universes)) else Univ.Instance.empty in let eq_projection_body p1 p2 = |