From fba1f0ed91aff372234b5a95422ee18f1730522f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 16 Dec 2014 10:58:13 +0100
Subject: Update checker/values and cic due to changes in case_info and
 record_body.

---
 checker/subtyping.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'checker/subtyping.ml')

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a9a037bce..0144580bc 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -198,7 +198,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let record_equal x y =
     match x, y with
     | None, None -> true
-    | Some (p1,pb1), Some (p2,pb2) ->
+    | Some None, Some None -> true
+    | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
+      Id.equal id1 id2 &&
       Array.for_all2 eq_con_chk p1 p2 &&
       Array.for_all2 eq_projection_body pb1 pb2
     | _, _ -> false
-- 
cgit v1.2.3