Remove the proj_body field from the kernel.

This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.

Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.

Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.

11 files changed, 40 insertions, 53 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 94958447e..3304b032e 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -211,7 +211,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
-  proj_body : constr; (* For compatibility, the match version *)
 }
 
 type constant_def =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6f9bf8fce..f4ae02084 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -130,7 +130,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> x.proj_body); true
+    true
   in
   let check_inductive_type t1 t2 =
 
diff --git a/checker/values.ml b/checker/values.ml
index 12fbf1ff0..45f04f88d 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 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli
+MD5 07651f61f86d91b22ff7056c6a8d86bc 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_constr|]
+    [|v_cst;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 abebec156..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,7 +54,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
-  proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
 (* Global declarations (i.e. constants) can be either: *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index fc6dc8b9e..1b73096f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -86,7 +86,7 @@ let subst_const_def sub def = match def with
 let subst_const_proj sub pb =
   { pb with proj_ind = subst_mind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
-    proj_body = subst_const_type sub pb.proj_body }
+  }
 
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4bc7ea198..14f2a3d8f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,16 +797,13 @@ exception UndefinableExpansion
     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 ((kn, _ as ind), u as indu) n x nparamargs params
+let compute_projections ((kn, _ as ind), u) nparamargs params
     mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
-  let indty, paramsletsubst =
-    (* [ty] = [Ind inst] is typed in context [params] *)
-    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
-    let ty = mkApp (mkIndU indu, inst) in
+  let paramsletsubst =
     (* [Ind inst] is typed in context [params-wo-let] *)
     let inst' = rel_list 0 nparamargs in
     (* {params-wo-let |- subst:params] *)
@@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst in
-      ty, subst
+    subst
   in
-  let ci = 
-    let print_info =
-      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-      { ci_ind     = ind;
-	ci_npar    = nparamargs;
-	ci_cstr_ndecls = mind_consnrealdecls;
-	ci_cstr_nargs = mind_consnrealargs;
-	ci_pp_info = print_info }
-  in
-  let len = List.length ctx in
-  let x = Name x in
-  let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:indty] *)
-    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
-    let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 indty, ccl') in
-    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
-    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
-  in
-  let projections decl (i, j, kns, pbs, subst, letsubst) =
+  let projections decl (i, j, kns, pbs, letsubst) =
     match decl with
     | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
         let c = liftn 1 j c in
         (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
-           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
-        let c1 = substl subst c in
-        (* From [params, x:I |- subst:field1,..,fieldj]
-           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
-           is represented with instance of field1 last *)
-        let subst = c1 :: subst in
-        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
         let c2 = substl letsubst c in
         (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
            to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
         let letsubst = c2 :: letsubst in
-        (i, j+1, kns, pbs, subst, letsubst)
+        (i, j+1, kns, pbs, letsubst)
     | LocalAssum (na,t) ->
       match na with
       | Name id ->
@@ -868,17 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
 	let projty = substl letsubst t in
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
-	let ty = substl subst t in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let compat = compat_body ty (j - 1) in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-                      proj_arg = i; proj_type = projty; proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs,
-	   fterm :: subst, fterm :: letsubst)
+                      proj_arg = i; proj_type = projty; } in
+        (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst, letsubst) =
-    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  let (_, _, kns, pbs, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
   in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
@@ -983,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
+             compute_projections indsp nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a38172c2..45228e35e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive -> Id.t -> Id.t ->
+val compute_projections : pinductive ->
   int -> Context.Rel.t -> int array -> int array -> 
   Context.Rel.t -> Context.Rel.t -> 
   (Constant.t array * projection_body array)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b1ee21536..3a61c7747 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,7 +1069,11 @@ let extract_constant env kn cb =
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_typ (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_typ (get_opaque env c)
@@ -1082,7 +1086,11 @@ let extract_constant env kn cb =
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_def (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_def (get_opaque env c)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..5a54c6f05 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t =
 	  let c' = 
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
-	      let body = pb.Declarations.proj_body in
+              (** FIXME: handle mutual records *)
+              let ind = (pb.Declarations.proj_ind, 0) 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
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4ad32fc66..1a790be64 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -549,6 +549,9 @@ let compute_projections env (kn, _ as ind) =
   in
   Array.rev_of_list pbs
 
+let legacy_match_projection env ind =
+  Array.map pi3 (compute_projections env ind)
+
 let compute_projections ind mib =
   let ans = compute_projections ind mib in
   Array.map (fun (prj, ty, _) -> (prj, ty)) ans
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 506cdd8c9..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -198,6 +198,14 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
 (** Given a primitive record type, for every field computes the eta-expanded
     projection and its type. *)
 
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+    projections.
+
+    BEWARE: such terms are ill-typed, and should thus only be used in upper
+    layers. The kernel will probably badly fail if presented with one of
+    those. *)
+
 (********************)
 
 val type_of_inductive_knowing_conclusion :