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

Fixes #6764: Printing Notation regressed compared to 8.7

6 files changed, 3 insertions, 34 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d8dd4ef6dd..77d612cfd9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -114,7 +114,6 @@ and constr_expr_r =
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
   | CDelimiters of string * constr_expr
-  | CProj of qualid * constr_expr
 and constr_expr = constr_expr_r CAst.t
 
 and case_expr = constr_expr                 (* expression that is being matched *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 011c4a6e4e..23d0536df8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -177,12 +177,10 @@ let rec constr_expr_eq e1 e2 =
     | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
-    | CProj(p1,c1), CProj(p2,c2) ->
-      qualid_eq p1 p2 && constr_expr_eq c1 c2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
      | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
-     | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
+     | CGeneralization _ | CDelimiters _ ), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -359,8 +357,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->
       Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
-    | CProj (_,c) ->
-        f n acc c
   )
 
 let free_vars_of_constr_expr c =
@@ -439,8 +435,6 @@ let map_constr_expr_with_binders g f e = CAst.map (function
           let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,bl',t',d')) dl)
-    | CProj (p,c) ->
-      CProj (p, f e c)
   )
 
 (* Used in constrintern *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3996a1756c..98e1f6dd36 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -958,9 +958,6 @@ let rec extern inctx scopes vars r =
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
-  | GProj (p, c) ->
-    let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
-    CProj (pr, sub_extern inctx scopes vars c)
 
   in insert_coercion coercion (CAst.make ?loc c)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1c8d957014..d02f59414e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2062,13 +2062,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CCast (c1, c2) ->
 	DAst.make ?loc @@
         GCast (intern env c1, map_cast_type (intern_type env) c2)
-    | CProj (pr, c) ->
-      match intern_reference pr with
-      | ConstRef p ->
-        let p = Option.get @@ Recordops.find_primitive_projection p in
-        DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
-      | _ ->
-        raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
     )
   and intern_type env = intern (set_type_scope env)
 
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
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 942ea5ff3f..5fb0ca1b43 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,7 +43,6 @@ type notation_constr =
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NCast of notation_constr * notation_constr cast_type
-  | NProj of Projection.t * notation_constr
 
 (** Note concerning NList: first constr is iterator, second is terminator;
     first id is where each argument of the list has to be substituted