Revert #6651: Use r.(p) syntax to print primitive projections

Fixes #6764: Printing Notation regressed compared to 8.7

3 files changed, 1 insertions, 11 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fd2d90e9cf..0c45de4dc4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -590,7 +590,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
-            | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
 	end (* end of the application treatement *)
 
@@ -696,7 +695,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
 	build_entry_lc env funnames  avoid b
-    | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
@@ -1246,7 +1244,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
 		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ | GProj _ ->
+  | GIf _ | GRec _ | GCast _ ->
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 954fc3bab4..f81de82d5e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,6 @@ let change_vars =
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
-      | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
   and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -294,7 +293,6 @@ let rec alpha_rt excluded rt =
 	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
 	    )
-    | GProj(p,c) -> GProj(p, alpha_rt excluded c)
   in
   new_rt
 
@@ -346,7 +344,6 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
-    | GProj (_,c) -> is_free_in c
     ) x
   and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -440,8 +437,6 @@ let replace_var_by_term x_id term =
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
-      | GProj(p,c) ->
-        GProj(p,replace_var_by_pattern c)
     ) x
   and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -545,7 +540,6 @@ let expand_as =
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
-      | GProj(p,c) -> GProj(p, expand_as map c)
     )
   and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
     CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e114a0119e..9eda19a86b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -222,7 +222,6 @@ let is_rec names =
     | GCases(_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
-    | GProj(_,c) -> lookup names c
   and lookup_br names {CAst.v=(idl,_,rt)} =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
@@ -783,7 +782,6 @@ let rec add_args id new_args = CAst.map (function
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
   | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
   | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
-  | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
   )
 exception Stop of  Constrexpr.constr_expr