Using more general information for primitive records.

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

5 files changed, 29 insertions, 21 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index ee7914f99..a890f2cef 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -252,9 +252,10 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
-    (* The body is empty for non-primitive records, otherwise we get its
-       binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
@@ -322,7 +323,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+    mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa8..2dcc1a984 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -619,7 +619,8 @@ let drop_parameters depth n argstk =
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.mind_record with
-    | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite -> 
+    | PrimRecord info when mib.mind_finite <> CoFinite ->
+      let (_, projs, pbs) = info.(snd ind) in
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.mind_nparams in
diff --git a/checker/environ.ml b/checker/environ.ml
index 3d5fac806..ba1eb0ddb 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -192,11 +192,12 @@ let add_mind kn mib env =
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let new_projections = match mib.mind_record with
-    | None | Some None -> env.env_globals.env_projections
-    | Some (Some (id, kns, pbs)) ->
-      Array.fold_left2 (fun projs kn pb ->
-          Cmap_env.add kn pb projs)
-        env.env_globals.env_projections kns pbs
+    | NotRecord | FakeRecord -> env.env_globals.env_projections
+    | PrimRecord projs ->
+      Array.fold_left (fun accu (id, kns, pbs) ->
+      Array.fold_left2 (fun accu kn pb ->
+          Cmap_env.add kn pb accu) accu kns pbs)
+        env.env_globals.env_projections projs
   in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
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)
diff --git a/checker/values.ml b/checker/values.ml
index c0ddc1908..4f28d6e44 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 2356846eddb0113e5e75bf8b46cddaee checker/cic.mli
+MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
 
 *)
 
@@ -274,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body"
     Any|]
 
 let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record", 
-			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+  v_sum "record_info" 2
+    [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0
@@ -283,7 +285,7 @@ let v_ind_pack_univs =
 
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
-    v_mind_record;
+    v_record_info;
     v_finite;
     Int;
     v_section_ctxt;