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

Fixes #6764: Printing Notation regressed compared to 8.7

1 files changed, 2 insertions, 15 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 06943ce7b9..ff5e2bb5f3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,11 +89,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   glob_sort_eq s1 s2
 | NCast (t1, c1), NCast (t2, c2) ->
   (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
-| NProj (p1, c1), NProj (p2, c2) ->
-  Projection.equal p1 p2 && eq_notation_constr vars c1 c2
 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
   | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
+  | NRec _ | NSort _ | NCast _ ), _ -> false
 
 (**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
@@ -220,7 +218,6 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
-  | NProj (p,c) -> GProj (p, f e c)
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
@@ -440,7 +437,6 @@ let notation_constr_and_vars_of_glob_constr recvars a =
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
   | GRef (r,_) -> NRef r
-  | GProj (p, c) -> NProj (p, aux c)
   | GEvar _ | GPatVar _ ->
       user_err Pp.(str "Existential variables not allowed in notations.")
   ) x
@@ -640,12 +636,6 @@ let rec subst_notation_constr subst bound raw =
       let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
-  | NProj (p, c) ->
-    let p' = subst_proj subst p in
-    let c' = subst_notation_constr subst bound c in
-    if p' == p && c' == c then raw else NProj(p', c')
-
-
 let subst_interpretation subst (metas,pat) =
   let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
   (metas,subst_notation_constr subst bound pat)
@@ -1218,12 +1208,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
 
-  | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
-    match_in u alp metas sigma t1 t2
-
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
-     | GCast _ | GProj _ ), _ -> raise No_match
+     | GCast _ ), _ -> raise No_match
 
 and match_in u = match_ true u