Merge PR #9306: Remove Printing Primitive Projection Compatibility

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 7 insertions, 72 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6746e4b902..99cd89cc2a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open CErrors
 open Util
@@ -175,16 +173,6 @@ let () = declare_bool_option
 	    optread  = print_primproj_params;
 	    optwrite = (:=) print_primproj_params_value }
 
-let print_primproj_compatibility_value = ref false
-let print_primproj_compatibility () = !print_primproj_compatibility_value
-
-let () = declare_bool_option
-	  { optdepr  = false;
-	    optname  = "backwards-compatible printing of primitive projections";
-	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
-	    optread  = print_primproj_compatibility;
-	    optwrite = (:=) print_primproj_compatibility_value }
-
 	  
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t =
 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), 
 		[detype d flags avoid env sigma c])
       else 
-	if print_primproj_compatibility () && Projection.unfolded p then
-          (* Print the compatibility match version *)
-	  let c' = 
-	    try 
-              let ind = Projection.inductive p in
-              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
-              let body = bodies.(Projection.arg p) 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
-	      let u = EInstance.kind sigma u in
-	      let body' = CVars.subst_instance_constr u body' in
-	      let body' = EConstr.of_constr body' in
-		substl (c :: List.rev args) body'
-	    with Retyping.RetypeError _ | Not_found -> 
-	      anomaly (str"Cannot detype an unfolded primitive projection.")
-	  in DAst.get (detype d flags avoid env sigma c')
-	else
-	  if print_primproj_params () then
-	    try
-	      let c = Retyping.expand_projection (snd env) sigma p c [] in
-              DAst.get (detype d flags avoid env sigma c)
-	    with Retyping.RetypeError _ -> noparams ()
-	  else noparams ()
+        if print_primproj_params () then
+          try
+            let c = Retyping.expand_projection (snd env) sigma p c [] in
+            DAst.get (detype d flags avoid env sigma c)
+          with Retyping.RetypeError _ -> noparams ()
+        else noparams ()
 
     | Evar (evk,cl) ->
         let bound_to_itself_or_letin decl c =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 2c4ca46343..4c02dc0f09 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -475,25 +475,6 @@ let compute_projections env (kn, i as ind) =
     (* [Ind inst] is typed in context [params-wo-let] *)
     ty
   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 = pkt.mind_consnrealdecls;
-        ci_cstr_nargs = pkt.mind_consnrealargs;
-        ci_pp_info = print_info }
-  in
-  let len = List.length ctx 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 (proj_arg, j, pbs, subst) =
     match decl with
     | LocalDef (na,c,t) ->
@@ -523,10 +504,9 @@ let compute_projections env (kn, i as ind) =
         let ty = substl subst t in
         let term = mkProj (Projection.make kn true, mkRel 1) in
         let fterm = mkProj (Projection.make kn false, mkRel 1) in
-        let compat = compat_body ty (j - 1) in
         let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
         let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
-        let body = (etab, etat, compat) in
+        let body = (etab, etat) in
         (proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
       | Anonymous ->
         anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -536,13 +516,6 @@ let compute_projections env (kn, i 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
-
 (**************************************************)
 
 let extract_mrectype sigma t =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b2e205115f..5a4257e175 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,14 +194,6 @@ 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 :