Merge PR #7750: Handle mutual records in the kernel

5 files changed, 24 insertions, 16 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fe49d64c7..23a985dc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t =
 	  let c' = 
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
-              (** FIXME: handle mutual records *)
-              let ind = (pb.Declarations.proj_ind, 0) in
+              let ind = pb.Declarations.proj_ind in
               let bodies = Inductiveops.legacy_match_projection (snd env) ind in
               let body = bodies.(pb.Declarations.proj_arg) in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d08f66c1..88a91af88 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+  let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+    | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+      let (_, projs, _) = info.(snd ind) in
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1003f86c5..d599afe69 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == BiFinite
-  | _ -> true
+  | PrimRecord _ -> mib.mind_finite == BiFinite
+  | NotRecord | FakeRecord -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
 let get_projections env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
     match mib.mind_record with
-    | Some (Some (id, projs, pbs)) -> Some projs
-    | _ -> None
+    | PrimRecord infos ->
+      let (_, projs, _) = infos.(snd (fst ind)) in
+      Some projs
+    | NotRecord | FakeRecord -> None
 
 let make_case_or_project env sigma indf ci pred c branches =
   let open EConstr in
@@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs =
     build an expansion function.
     The term built is expecting to be substituted first by
     a substitution of the form [params, x : ind params] *)
-let compute_projections env (kn, _ as ind) =
+let compute_projections env (kn, i as ind) =
   let open Term in
   let mib = Environ.lookup_mind kn env in
   let indu = match mib.mind_universes with
@@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) =
     mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
   in
   let x = match mib.mind_record with
-  | None | Some None ->
+  | NotRecord | FakeRecord ->
     anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
-  | Some (Some (id, _, _)) -> Name id
+  | PrimRecord info-> Name (pi1 (info.(i)))
   in
   (** FIXME: handle mutual records *)
   let pkt = mib.mind_packets.(0) in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..7319846fb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs =
     bs ci in
   Array.init (Array.length tbl) branch
 
-let get_proj env ((mind, _n), i) =
+let get_proj env ((mind, n), i) =
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
-  | None | Some None ->
+  | NotRecord | FakeRecord ->
     CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
-  | Some (Some (_, projs, _)) ->
+  | PrimRecord info ->
+    let _, projs, _ = info.(n) in
     Projection.make projs.(i) true
 
 let rec nf_val env sigma v typ =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
 
 let is_eta_constructor_app env sigma ts f l1 term =
   match EConstr.kind sigma f with
-  | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+  | Construct (((_, i as ind), j), u) when j == 1 ->
+    let open Declarations in
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+      | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+          let (_, projs, _) = info.(i) in
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env sigma ts term
@@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term =
   | _ -> false
 
 let eta_constructor_app env sigma f l1 term =
+  let open Declarations in
   match EConstr.kind sigma f with
   | Construct (((_, i as ind), j), u) ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_, projs, _)) ->
+      | PrimRecord info ->
+        let (_, projs, _) = info.(i) in
         let npars = mib.Declarations.mind_nparams in
 	let pars, l1' = Array.chop npars l1 in
 	let arg = Array.append pars [|term|] in