From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 2 May 2017 19:53:05 +0200 Subject: Correct coqchk reduction --- checker/subtyping.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker/subtyping.ml') 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 = -- cgit v1.2.3