Change the proj_ind field from MutInd.t to inductive.

This is a first step towards the acceptance of mutual record types in the
kernel.

12 files changed, 16 insertions, 19 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 3304b032e..ee7914f99 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -207,7 +207,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : MutInd.t;
+  proj_ind : inductive;
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index f4ae02084..6a051a5a9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -126,7 +126,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check MutInd.equal (fun x -> x.proj_ind);
+    check eq_ind (fun x -> x.proj_ind);
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b..345ee5b8f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(MutInd.equal pb.proj_ind (fst ind));
+    assert(eq_ind pb.proj_ind ind);
     let ty = subst_instance_constr u pb.proj_type in
       substl (c :: List.rev args) ty
 
diff --git a/checker/values.ml b/checker/values.ml
index 31e65729b..c0ddc1908 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 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
+MD5 2356846eddb0113e5e75bf8b46cddaee checker/cic.mli
 
 *)
 
@@ -225,7 +225,7 @@ let v_cst_def =
 
 let v_projbody =
   v_tuple "projection_body"
-    [|v_cst;Int;Int;v_constr|]
+    [|v_ind;Int;Int;v_constr|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd7d6c9c..bb81f7514 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,7 +50,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : MutInd.t;
+  proj_ind : inductive;
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1b73096f7..ad5167d8b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,7 +84,7 @@ let subst_const_def sub def = match def with
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
 let subst_const_proj sub pb =
-  { pb with proj_ind = subst_mind sub pb.proj_ind;
+  { pb with proj_ind = subst_ind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
   }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 14f2a3d8f..5b3bca3a0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -839,7 +839,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let body = { proj_ind = fst ind; proj_npars = nparamargs;
+        let body = { proj_ind = ind; proj_npars = nparamargs;
                       proj_arg = i; proj_type = projty; } in
         (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8257dc8b8..914168695 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1965,6 +1965,7 @@ let compile_mind prefix ~interactive mb mind stack =
     in
     let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
     let add_proj j acc pb =
+      let () = assert (eq_ind ind pb.proj_ind) in
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
@@ -1985,7 +1986,7 @@ let compile_mind prefix ~interactive mb mind stack =
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
       let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
-      let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in
+      let gn = Gproj ("", ind, pb.proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
     let projs = match mb.mind_record with
@@ -2052,7 +2053,7 @@ let compile_deps env sigma prefix ~interactive init t =
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let pb = lookup_projection p env in
-    let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in
+    let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in
     aux env lvl init c
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 0325a00b4..a809e1b18 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -520,8 +520,7 @@ let rec lambda_of_constr env sigma c =
 
   | Proj (p, c) ->
     let pb = lookup_projection p !global_env in
-    (** FIXME: handle mutual records *)
-    let ind = (pb.proj_ind, 0) in
+    let ind = pb.proj_ind in
     let prefix = get_mind_prefix !global_env (fst ind) in
     mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|]
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 325d5cecd..34ed2afb2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,7 +301,7 @@ let type_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(MutInd.equal pb.proj_ind (fst ind));
+  assert(eq_ind pb.proj_ind ind);
   let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
   substl (c :: CList.rev args) ty
       
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3a61c7747..bbf56525a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,8 +1069,7 @@ let extract_constant env kn cb =
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) 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 env ind in
                 let body = bodies.(pb.Declarations.proj_arg) in
                 mk_typ (EConstr.of_constr body))
@@ -1086,8 +1085,7 @@ let extract_constant env kn cb =
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) 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 env ind in
                 let body = bodies.(pb.Declarations.proj_arg) in
                 mk_def (EConstr.of_constr body))
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