Using more general information for primitive records.

This brings more compatibility with handling of mutual primitive records
in the kernel.

1 files changed, 10 insertions, 7 deletions

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6a051a5a9..a22af4e0f 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -218,16 +218,19 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   (* we check that records and their field names are preserved. *)
   let record_equal x y =
     match x, y with
-    | None, None -> true
-    | Some None, Some None -> true
-    | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
-      Id.equal id1 id2 &&
-      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-      Array.for_all2 eq_projection_body pb1 pb2
+    | NotRecord, NotRecord -> true
+    | FakeRecord, FakeRecord -> true
+    | PrimRecord info1, PrimRecord info2 ->
+      let check (id1, p1, pb1) (id2, p2, pb2) =
+        Id.equal id1 id2 &&
+        Array.for_all2 Constant.UserOrd.equal p1 p2 &&
+        Array.for_all2 eq_projection_body pb1 pb2
+      in
+      Array.equal check info1 info2
     | _, _ -> false
   in
   check record_equal (fun mib -> mib.mind_record);
-  if mib1.mind_record != None then begin
+  if mib1.mind_record != NotRecord then begin
     let rec names_prod_letin t = match t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)