diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-05-02 19:53:05 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:17 +0200 |
| commit | d6898781f9cd52ac36a4891d7b169ddab7b8af50 (patch) | |
| tree | 880ef0bcad043f083a6157644d10e068b8185b4c /checker/subtyping.ml | |
| parent | 4bf85270a36a0a3f9517d8bce92d843f882af00a (diff) | |
Correct coqchk reduction
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 = |