diff --git a/dev/ci/user-overlays/14598-herbelin-master+proj-nodes-in-concrete-syntax.sh b/dev/ci/user-overlays/14598-herbelin-master+proj-nodes-in-concrete-syntax.sh
new file mode 100644
index 000000000000..6342dfacfb07
--- /dev/null
+++ b/dev/ci/user-overlays/14598-herbelin-master+proj-nodes-in-concrete-syntax.sh
@@ -0,0 +1,2 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr14598-adding-proj-syntax-constructor 14598
+overlay quickchick https://github.com/herbelin/QuickChick master+adapt-coq-pr14598-adding-proj-syntax-constructor 14598
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1396609b7e51..0cb8a2af4db7 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,14 @@
 
 - Renaming `LSet` into `Level.Set` and `LMap` into `Level.Map`
 
+### Concrete syntax
+
+- Explicit nodes `CProj` and `GProj` have been added for the syntax of
+  projections `t.(f)` in `constr_expr` and `glob_constr`, while they
+  were previously encoded in the `CApp` and `GApp` nodes. There may be
+  a need for adding a new case in pattern-matching. The types of `CApp`
+  and `CAppExpl` have been simplified accordingly.
+
 ## Changes between Coq 8.13 and Coq 8.14
 
 ### Build system and library infrastructure
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 72ffac5bf339..0082f4d95ae1 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -177,8 +177,8 @@ Syntax of Record Projections
   .. insertprodn term_projection term_projection
 
   .. prodn::
-     term_projection ::= @term0 .( @qualid {* @arg } )
-     | @term0 .( @ @qualid {* @term1 } )
+     term_projection ::= @term0 .( @qualid {? @univ_annot } {* @arg } )
+     | @term0 .( @ @qualid {? @univ_annot } {* @term1 } )
 
 The corresponding grammar rules are given in the preceding grammar. When :token:`qualid`
 denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`,
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 807d02327d23..9f0f879b7997 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -401,13 +401,13 @@ term9: [
 ]
 
 term1: [
-| REPLACE term0 ".(" global LIST0 arg ")"
-| WITH    term0 ".(" global LIST0 arg ")" (* huh? *)
+| REPLACE term0 ".(" global univ_annot LIST0 arg ")"
+| WITH    term0 ".(" global univ_annot LIST0 arg ")" (* huh? *)
 | REPLACE term0 "%" IDENT
 | WITH term0 "%" scope_key
 | MOVETO term_scope term0 "%" scope_key
-| MOVETO term_projection term0 ".(" global LIST0 arg ")"
-| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")"
+| MOVETO term_projection term0 ".(" global univ_annot LIST0 arg ")"
+| MOVETO term_projection term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
 ]
 
 term0: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 3f62c3aa6903..6901d46b0dfa 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -103,8 +103,8 @@ term8: [
 ]
 
 term1: [
-| term0 ".(" global LIST0 arg ")"
-| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 ".(" global univ_annot LIST0 arg ")"
+| term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
 | term0 "%" IDENT
 | term0
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 9edbf2cb8ae8..54c6f4c9d57a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -55,8 +55,8 @@ term_ltac: [
 ]
 
 term_projection: [
-| term0 ".(" qualid LIST0 arg ")"
-| term0 ".(" "@" qualid LIST0 ( term1 ) ")"
+| term0 ".(" qualid OPT univ_annot LIST0 arg ")"
+| term0 ".(" "@" qualid OPT univ_annot LIST0 ( term1 ) ")"
 ]
 
 term_scope: [
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index b14c325f6907..65a6a3202b25 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -71,7 +71,7 @@ type binder_kind =
 
 type abstraction_kind = AbsLambda | AbsPi
 
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+type explicit_flag = bool (** true = with "@" *)
 
 type prim_token =
   | Number of NumTok.Signed.t
@@ -108,9 +108,10 @@ and constr_expr_r =
   | CProdN   of local_binder_expr list * constr_expr
   | CLambdaN of local_binder_expr list * constr_expr
   | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
-  | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
-  | CApp     of (proj_flag * constr_expr) *
-                (constr_expr * explicitation CAst.t option) list
+  | CAppExpl of (qualid * instance_expr option) * constr_expr list
+  | CApp     of constr_expr * (constr_expr * explicitation CAst.t option) list
+  | CProj    of explicit_flag * (qualid * instance_expr option)
+              * (constr_expr * explicitation CAst.t option) list * constr_expr
   | CRecord  of (qualid * constr_expr) list
 
   (* representation of the "let" and "match" constructs *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 1960ecfd3c8e..485530a53c00 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -141,15 +141,19 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
-    | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) ->
-      Option.equal Int.equal proj1 proj2 &&
+    | CAppExpl((r1,u1),al1), CAppExpl((r2,u2),al2) ->
       qualid_eq r1 r2 &&
       eq_universes u1 u2 &&
       List.equal constr_expr_eq al1 al2
-    | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
-      Option.equal Int.equal proj1 proj2 &&
+    | CApp(e1,al1), CApp(e2,al2) ->
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
+    | CProj(e1,(p1,u1),al1,c1), CProj(e2,(p2,u2),al2,c2) ->
+      e1 = (e2:bool) &&
+      qualid_eq p1 p2 &&
+      eq_universes u1 u2 &&
+      List.equal args_eq al1 al2 &&
+      constr_expr_eq c1 c2
     | CRecord l1, CRecord l2 ->
       let field_eq (r1, e1) (r2, e2) =
         qualid_eq r1 r2 && constr_expr_eq e1 e2
@@ -199,7 +203,7 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 &&
       eq_universes u1 u2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
-     | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
+     | CApp _ | CProj _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
      | CGeneralization _ | CDelimiters _ | CArray _), _ -> false
 
@@ -338,8 +342,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function
     f n acc b
 
 let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
-    | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
-    | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+    | CAppExpl ((_,_),l) -> List.fold_left (f n) acc l
+    | CApp (t,l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+    | CProj (e,_,l,t) -> f n (List.fold_left (f n) acc (List.map fst l)) t
     | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
@@ -447,8 +452,10 @@ let fold_map_local_binders f g e bl =
 
 let map_constr_expr_with_binders g f e = CAst.map (function
     | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
-    | CApp ((p,a),l) ->
-      CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
+    | CApp (a,l) ->
+      CApp (f e a,List.map (fun (a,i) -> (f e a,i)) l)
+    | CProj (expl,p,l,a) ->
+      CProj (expl,p,List.map (fun (a,i) -> (f e a,i)) l,f e a)
     | CProdN (bl,b) ->
       let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
@@ -585,7 +592,7 @@ let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
   match CAst.(f.v) with
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
-  | _           -> CAst.make @@ CApp ((None, f), l)
+  | _           -> CAst.make @@ CApp (f, l)
 
 let mkProdCN ?loc bll c =
   if bll = [] then c else
@@ -647,9 +654,9 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
   | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
       when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
       CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
-  | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
+  | CApp (p,args) when List.for_all (fun (_,e) -> e=None) args ->
      (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
-  | CAppExpl ((None,r,i),args) ->
+  | CAppExpl ((r,i),args) ->
      CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
   | CNotation (inscope,ntn,(c,cl,[],[])) ->
      CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bafc9b40e710..7c09077c7f26 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -688,16 +688,17 @@ let adjust_implicit_arguments inctx n args impl =
     | [], _ -> []
   in exprec (args,impl)
 
-let extern_projection inctx f i args impl =
-  let (args1,args2) = List.chop i args in
-  let nexpectedparams = i - 1 in
+let extern_projection inctx f nexpectedparams args impl =
+  let (args1,args2) = List.chop (nexpectedparams + 1) args in
   let nextraargs = List.length args2 in
   let (impl1,impl2) = impargs_for_proj ~nexpectedparams ~nextraargs impl in
   let n = nexpectedparams + 1 + nextraargs in
   let args1 = adjust_implicit_arguments inctx n args1 impl1 in
   let args2 = adjust_implicit_arguments inctx n args2 impl2 in
-  let ip = Some (List.length args1) in
-  CApp ((ip,f),args1@args2)
+  let (c1,expl), args1 = List.sep_last args1 in
+  assert (expl = None);
+  let c = CProj (false,f,args1,c1) in
+  if args2 = [] then c else CApp (CAst.make c, args2)
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -746,14 +747,13 @@ let extern_record ref args =
 let extern_global impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
-    CAppExpl ((None, f, us), [])
+    CAppExpl ((f, us), [])
   else
     CRef (f,us)
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let extern_applied_ref inctx impl (cf,f) us args =
-  let isproj = is_projection (List.length args) cf in
   try
     if not !Constrintern.parsing_explicit &&
        ((!Flags.raw_print ||
@@ -763,30 +763,37 @@ let extern_applied_ref inctx impl (cf,f) us args =
     let impl = if !Constrintern.parsing_explicit then [] else impl in
     let n = List.length args in
     let ref = CRef (f,us) in
-    let f = CAst.make ref in
+    let r = CAst.make ref in
     let ip = is_projection n cf in
     match ip with
     | Some i ->
       (* [t.(f args1) args2] projection-style notation *)
-      extern_projection inctx f i args impl
+      extern_projection inctx (f,us) (i-1) args impl
     | None ->
       let args = adjust_implicit_arguments inctx n args impl in
-      if args = [] then ref else CApp ((None, f), args)
+      if args = [] then ref else CApp (r, args)
   with Expl ->
   (* A [@f args] node *)
     let args = List.map Lazy.force args in
-    let isproj = if !print_projections then isproj else None in
-    CAppExpl ((isproj,f,us), args)
+    match is_projection (List.length args) cf with
+    | Some n when !print_projections ->
+       let args = List.map (fun c -> (c,None)) args in
+       let args1, args2 = List.chop n args in
+       let (c1,_), args1 = List.sep_last args1 in
+       let c = CProj (true, (f,us), args1, c1) in
+       if args2 = [] then c else CApp (CAst.make c, args2)
+    | _ ->
+       CAppExpl ((f,us), args)
 
 let extern_applied_syntactic_definition inctx n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
     let extraargs = adjust_implicit_arguments inctx n extraargs extraimpl in
     let args = syndefargs @ extraargs in
-    if args = [] then cf else CApp ((None, CAst.make cf), args)
+    if args = [] then cf else CApp (CAst.make cf, args)
   with Expl ->
     let args = syndefargs @ List.map Lazy.force extraargs in
-    CAppExpl ((None,f,None), args)
+    CAppExpl ((f,None), args)
 
 let mkFlattenedCApp (head,args) =
   match head.CAst.v with
@@ -795,7 +802,7 @@ let mkFlattenedCApp (head,args) =
     (* or after removal of a coercion to funclass *)
     CApp (g,args'@args)
   | _ ->
-    CApp ((None, head), args)
+    CApp (head, args)
 
 let extern_applied_notation inctx n impl f args =
   if List.is_empty args then
@@ -1039,11 +1046,16 @@ let rec extern inctx ?impargs scopes vars r =
                extern_applied_ref inctx
                  (select_stronger_impargs (implicits_of_global ref))
                  (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args)
+         | GProj (f,params,c) ->
+             extern_applied_proj inctx scopes vars f params c args
          | _ ->
              let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
              let head = sub_extern false scopes vars f in
              mkFlattenedCApp (head,args))
 
+  | GProj (f,params,c) ->
+      extern_applied_proj inctx scopes vars f params c []
+
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
               Option.map (extern_typ scopes vars) t,
@@ -1391,6 +1403,18 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
       with
           No_match -> extern_notation inctx allscopes vars t rules
 
+and extern_applied_proj inctx scopes vars (cst,us) params c extraargs =
+  let ref = GlobRef.ConstRef cst in
+  let subscopes = find_arguments_scope ref in
+  let nparams = List.length params in
+  let args = params @ c :: extraargs in
+  let args = fill_arg_scopes args subscopes scopes in
+  let args = extern_args (extern true) vars args in
+  let imps = select_stronger_impargs (implicits_of_global ref) in
+  let f = extern_reference (fst vars) ref in
+  let us = extern_instance (snd vars) us in
+  extern_projection inctx (f,us) nparams args imps
+
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index db4aa39b75de..1cf08e73c9e9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -544,7 +544,7 @@ let intern_generalized_binder intern_type ntnvars
     | Anonymous ->
       let id =
         match ty with
-        | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+        | { v = CApp ({ v = CRef (qid,_) }, _) } when qualid_is_ident qid ->
           qualid_basename qid
         | _ -> default_non_dependent_ident
       in
@@ -806,7 +806,7 @@ let terms_of_binders bl =
        let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
-       CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
+       CAppExpl ((qid,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
     | bnd :: l ->
       let loc = bnd.loc in
@@ -842,7 +842,7 @@ let rec adjust_env env = function
   | NCast (c,_) -> adjust_env env c
   | NApp _ -> restart_no_binders env
   | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _
-  | NRec _ | NSort _ | NInt _ | NFloat _ | NArray _
+  | NRec _ | NSort _ | NProj _ | NInt _ | NFloat _ | NArray _
   | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
 
 let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
@@ -1217,6 +1217,13 @@ let find_appl_head_data env (_,ntnvars) c =
        List.skipn_at_least n scopes
     | _ -> [],[]
     end
+  | GProj ((cst,_), l, c) ->
+      let ref = GlobRef.ConstRef cst in
+      let n = List.length l + 1 in
+      let impls = implicits_of_global ref in
+      let scopes = find_arguments_scope ref in
+      List.map (drop_first_implicits n) impls,
+      List.skipn_at_least n scopes
   | _ -> [],[]
 
 let error_not_enough_arguments ?loc =
@@ -1944,17 +1951,19 @@ let get_implicit_name n imps =
 
 let set_hole_implicit i b c =
   let loc = c.CAst.loc in
-  match DAst.get c with
-  | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
+  let loc, r = match DAst.get c with
+  | GRef (r, _) -> loc, r
   | GApp (r, _) ->
     let loc = r.CAst.loc in
     begin match DAst.get r with
-    | GRef (r, _) ->
-      Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
+    | GRef (r, _) -> loc, r
+    | GProj ((cst,_), _, _) -> (* Improve: *) loc, GlobRef.ConstRef cst
     | _ -> anomaly (Pp.str "Only refs have implicits.")
     end
-  | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (GlobRef.VarRef id,i,b),IntroAnonymous,None)
-  | _ -> anomaly (Pp.str "Only refs have implicits.")
+  | GProj ((cst,_), _, _) -> loc, GlobRef.ConstRef cst
+  | GVar id -> loc, GlobRef.VarRef id
+  | _ -> anomaly (Pp.str "Only refs have implicits.") in
+  Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
 
 let exists_implicit_name id =
   List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp))
@@ -2115,9 +2124,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CDelimiters (key, e) ->
         intern {env with tmp_scope = None;
                   scopes = find_delimiters_scope ?loc key :: env.scopes} e
-    | CAppExpl ((Some n,ref,us), args) ->
-        intern_proj ?loc env true (ref,us) (List.map (fun c -> (c,None)) args) n []
-    | CAppExpl ((None,ref,us), args) ->
+    | CProj (expl, f, args, c) ->
+        intern_proj ?loc env expl f args c []
+    | CAppExpl ((ref,us), args) ->
         let f,args =
           let args = List.map (fun a -> (a,None)) args in
           intern_applied_reference ~isproj:false intern env (Environ.named_context_val globalenv)
@@ -2126,22 +2135,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         check_not_notation_variable f ntnvars;
         let _,args_scopes = find_appl_head_data env lvar f in
         (* Rem: GApp(_,f,[]) stands for @f *)
-        if args = [] then DAst.make ?loc @@ GApp (f,[]) else
-          smart_gapp f loc (intern_args env args_scopes (List.map fst args))
-
-    | CApp ((Some n,f), args) ->
-      (match f.CAst.v with
-        (* Compact notations like "t.(f args') args" *)
-        | CRef (ref,us) ->
-          intern_proj ?loc env false (ref,us) args n []
-        | _ -> assert false)
-
-    | CApp ((None,f), args) ->
-      (match f.CAst.v with
-        (* Compact notations like "t.(f args') args" *)
-        | CApp ((Some n,{v=CRef (ref,us);loc=locqid}), args') ->
-          intern_proj ?loc env false (ref,us) args' n args
-        (* Don't compact "(f args') args" to resolve implicits separately *)
+        let args = intern_args env args_scopes (List.map fst args) in
+        if args = [] then DAst.make ?loc @@ GApp (f,[])
+        else smart_gapp f loc args
+    | CApp (f, args) ->
+        begin match f.CAst.v with
+         (* t.(f args') args *)
+        | CProj (expl, (ref,us), args', c) ->
+          intern_proj ?loc:f.CAst.loc env expl (ref,us) args' c args
         | CRef (ref,us) ->
           let f, args = intern_applied_reference ~isproj:false intern env
             (Environ.named_context_val globalenv) lvar us args ref in
@@ -2153,8 +2154,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           let f = intern_no_implicit env f in
           let _, args_scopes = find_appl_head_data env lvar f in
           let args = extract_regular_arguments args in
-          smart_gapp f loc (intern_args env args_scopes args))
-
+          smart_gapp f loc (intern_args env args_scopes args)
+        end
     | CRecord fs ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
@@ -2409,10 +2410,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       (Id.Set.empty,Id.Map.empty,[]), None in
     (tm',(na.CAst.v, typ)), extra_id, match_td
 
-  and intern_proj ?loc env expl (qid,us) args1 n args2 =
-    let args1, args1' = List.chop n args1 in
-    let c, args1 = List.sep_last args1 in
-    let args2 = args1'@args2 in
+  and intern_proj ?loc env expl (qid,us) args1 c args2 =
     let f,args1 =
       intern_applied_reference ~isproj:true intern env
         (Environ.named_context_val globalenv) lvar us args1 qid
@@ -2437,16 +2435,16 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                            str (String.plural n " explicit parameter") ++ str ".")
       in
       let subscopes1, subscopes2 = List.chop (nexpectedparams + 1) subscopes in
-      let c,args1 = List.sep_last (intern_impargs f env imps1 subscopes1 (args1@[c])) in
-      let p = DAst.make ?loc:qid.CAst.loc (GRef (GlobRef.ConstRef p,us)) in
+      let c,args1 = List.sep_last (intern_impargs f env imps1 subscopes1 (args1@[c,None])) in
+      let p = DAst.make ?loc (GProj ((p,us),args0@args1,c)) in
       let args2 = intern_impargs p env imps2 subscopes2 args2 in
-      smart_gapp p loc (args0@args1@c::args2)
+      smart_gapp p loc args2
     | None ->
       (* Tolerate a use of t.(f) notation for an ordinary application until a decision is taken about it *)
-      if expl then intern env (CAst.make ?loc (CAppExpl ((None,qid,us), List.map fst (args1@c::args2))))
-      else intern env (CAst.make ?loc (CApp ((None,CAst.make ?loc:qid.CAst.loc (CRef (qid,us))), args1@c::args2)))
+      if expl then intern env (CAst.make ?loc (CAppExpl ((qid,us), List.map fst args1@c::List.map fst args2)))
+      else intern env (CAst.make ?loc (CApp ((CAst.make ?loc:qid.CAst.loc (CRef (qid,us))), args1@(c,None)::args2)))
 
- and intern_impargs c env l subscopes args =
+  and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
     if !parsing_explicit then
       if Id.Map.is_empty eargs then intern_args env subscopes rargs
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index ee07fb6ed1ff..d2d7e884cc05 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -178,7 +178,7 @@ let destClassAppExpl cl =
   let open CAst in
   let loc = cl.loc in
   match cl.v with
-    | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst)
+    | CApp ({ v = CRef (ref, inst) }, l) -> CAst.make ?loc (ref, l, inst)
     | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
     | _ -> raise Not_found
 
@@ -200,7 +200,7 @@ let implicit_application env ty =
     let sigma = Evd.from_env env in
     let c = class_info env sigma gr in
     let args, avoid = combine_params avoid par (List.rev c.cl_context) in
-    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
+    CAst.make ?loc @@ CAppExpl ((id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/notation.ml b/interp/notation.ml
index 2babe6979a37..9806629e9372 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -380,6 +380,7 @@ let glob_prim_constr_key c = match DAst.get c with
     | GRef (ref, _) -> Some (canonical_gr ref)
     | _ -> None
     end
+  | GProj ((cst,_), _, _) -> Some (canonical_gr (GlobRef.ConstRef cst))
   | _ -> None
 
 let glob_constr_keys c = match DAst.get c with
@@ -388,6 +389,7 @@ let glob_constr_keys c = match DAst.get c with
     | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth]
     | _ -> [Oth]
     end
+  | GProj ((cst,_), _, _) -> [RefKey (canonical_gr (GlobRef.ConstRef cst))]
   | GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | _ -> [Oth]
 
@@ -397,6 +399,7 @@ let cases_pattern_key c = match DAst.get c with
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
+  | NProj ((cst,_),args,_) -> RefKey(canonical_gr (GlobRef.ConstRef cst)), AppBoundedNotation (List.length args + 1)
   | NList (_,_,NApp (NRef (ref,_),args),_,_)
   | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 313a9e85a432..97131b4806cd 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -150,6 +150,9 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
     (* it had to be a single iteration of iter1 *)
     aux vars renaming tail1 t2
   | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
+  | NProj ((cst1,u1), l1, a1), NProj ((cst2,u2), l2, a2)
+    when GlobRef.equal (GlobRef.ConstRef cst1) (GlobRef.ConstRef cst2) && compare_glob_universe_instances lt strictly_lt u1 u2 ->
+    List.iter2 (aux vars renaming) l1 l2; aux vars renaming a1 a2
   | NLambda (na1, t1, u1), NLambda (na2, t2, u2)
   | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
     (match t1, t2 with
@@ -211,7 +214,7 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
     Array.iter2 (aux vars renaming) t1 t2;
     aux vars renaming def1 def2;
     aux vars renaming ty1 ty2
-  | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+  | (NRef _ | NVar _ | NApp _ | NProj _ | NHole _ | NList _ | NLambda _ | NProd _
     | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
     | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in
   try
@@ -327,6 +330,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
   | NApp (a,args) -> let e = h.no e in DAst.get (mkGApp (f e a) (List.map (f e) args))
+  | NProj (p,args,c) -> let e = h.no e in GProj (p, List.map (f e) args, f e c)
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
       let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
@@ -600,6 +604,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GApp (g,args) ->
      (* Treat applicative notes as binary nodes *)
      let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
+  | GProj (p,args,c) -> NProj (p, List.map aux args, aux c)
   | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c)
   | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c)
   | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
@@ -742,6 +747,15 @@ let rec subst_notation_constr subst bound raw =
         if r' == r && rl' == rl then raw else
           NApp(r',rl')
 
+  | NProj ((cst,u),rl,r) ->
+      let ref = GlobRef.ConstRef cst in
+      let ref',t = subst_global subst ref in
+      assert (t = None);
+      let rl' = List.Smart.map (subst_notation_constr subst bound) rl
+      and r' = subst_notation_constr subst bound r in
+        if ref' == ref && rl' == rl && r' == r then raw else
+          NProj ((destConstRef ref',u),rl',r')
+
   | NList (id1,id2,r1,r2,b) ->
       let r1' = subst_notation_constr subst bound r1
       and r2' = subst_notation_constr subst bound r2 in
@@ -1374,6 +1388,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_hd u alp metas sigma f1 f2) l1 l2
+  | GProj ((cst1,u1),l1,a1), NProj ((cst2,u2),l2,a2) when GlobRef.equal (GlobRef.ConstRef cst1) (GlobRef.ConstRef cst2) && compare_glob_universe_instances_le u1 u2 ->
+     match_in u alp metas (List.fold_left2 (match_in u alp metas) sigma l1 l2) a1 a2
+  | GApp (f1,l1), NProj ((cst2,u2),l2,a2) ->
+     (match DAst.get f1 with
+     | GRef (r1,u1) when GlobRef.equal r1 (GlobRef.ConstRef cst2) && compare_glob_universe_instances_le u1 u2 &&
+         List.length l1 = List.length l2 + 1 ->
+        List.fold_left2 (match_in u alp metas) sigma l1 (l2@[a2])
+     | _ -> raise No_match)
   | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) ->
      match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
   | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) ->
@@ -1469,7 +1491,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       Array.fold_left2 (match_in u alp metas) sigma t nt
     else raise No_match
 
-  | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
+  | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GProj _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
      | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index ec7165f854dc..fd6290d84571 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -24,6 +24,7 @@ type notation_constr =
   | NRef of GlobRef.t * glob_level list option
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
+  | NProj of (Constant.t * glob_level list option) * notation_constr list * notation_constr
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   (* Part only in [glob_constr] *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 649ba8b43379..13cefa07af8a 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -140,7 +140,7 @@ GRAMMAR EXTEND Gram
   ;
   constr:
     [ [ c = term LEVEL "8" -> { c }
-      | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
+      | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((f,i),[]) } ] ]
   ;
   term:
     [ "200" RIGHTA
@@ -155,22 +155,22 @@ GRAMMAR EXTEND Gram
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp((None,f),args) }
-      | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
+      [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp(f,args) }
+      | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((f,i),args) }
       | "@"; lid = pattern_ident; args = LIST1 identref ->
         { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
-          CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
+          CAst.make ~loc @@ CApp(CAst.make ?loc:locid @@ CPatVar id,args) } ]
     | "9"
       [ ".."; c = term LEVEL "0"; ".." ->
-        { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
+        { CAst.make ~loc @@ CAppExpl ((qualid_of_ident ~loc ldots_var, None),[c]) } ]
     | "8" [ ]
     | "1" LEFTA
-      [ c = term; ".("; f = global; args = LIST0 arg; ")" ->
-        { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
-      | c = term; ".("; "@"; f = global;
+      [ c = term; ".("; f = global; i = univ_annot; args = LIST0 arg; ")" ->
+        { CAst.make ~loc @@ CProj(false, (f,i), args, c) }
+      | c = term; ".("; "@"; f = global; i = univ_annot;
         args = LIST0 (term LEVEL "9"); ")" ->
-        { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) }
+        { CAst.make ~loc @@ CProj(true, (f,i), List.map (fun a -> (a,None)) args, c) }
       | c = term; "%"; key = IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
     | "0"
       [ c = atomic_constr -> { c }
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 2fae5182d197..747ccc151155 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -103,7 +103,7 @@ let is_rec names =
               (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
               names nal)
            b
-    | GApp (f, args) -> List.exists (lookup names) (f :: args)
+    | GApp (c, args) | GProj (_, args, c) -> List.exists (lookup names) (c :: args)
     | GArray (_u, t, def, ty) ->
       Array.exists (lookup names) t || lookup names def || lookup names ty
     | GCases (_, _, el, brl) ->
@@ -1660,7 +1660,7 @@ let register_wf interactive_proof ?(is_mes = false) fname rec_impls wf_rel_expr
     let f_app_args =
       CAst.make
       @@ Constrexpr.CAppExpl
-           ( (None, Libnames.qualid_of_ident fname, None)
+           ( (Libnames.qualid_of_ident fname, None)
            , List.map
                (function
                  | {CAst.v = Anonymous} -> assert false
@@ -1669,7 +1669,7 @@ let register_wf interactive_proof ?(is_mes = false) fname rec_impls wf_rel_expr
     in
     CAst.make
     @@ Constrexpr.CApp
-         ( (None, Constrexpr_ops.mkRefC (Libnames.qualid_of_string "Logic.eq"))
+         ( Constrexpr_ops.mkRefC (Libnames.qualid_of_string "Logic.eq")
          , [(f_app_args, None); (body, None)] )
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -1951,7 +1951,7 @@ let rec add_args id new_args =
   CAst.map (function
     | CRef (qid, _) as b ->
       if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
-        CAppExpl ((None, qid, None), new_args)
+        CAppExpl ((qid, None), new_args)
       else b
     | CFix _ | CCoFix _ -> CErrors.anomaly ~label:"add_args " (Pp.str "todo.")
     | CProdN (nal, b1) ->
@@ -1990,15 +1990,20 @@ let rec add_args id new_args =
         , add_args id new_args b1
         , Option.map (add_args id new_args) t
         , add_args id new_args b2 )
-    | CAppExpl ((pf, qid, us), exprl) ->
+    | CAppExpl ((qid, us), exprl) ->
       if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
         CAppExpl
-          ((pf, qid, us), new_args @ List.map (add_args id new_args) exprl)
-      else CAppExpl ((pf, qid, us), List.map (add_args id new_args) exprl)
-    | CApp ((pf, b), bl) ->
+          ((qid, us), new_args @ List.map (add_args id new_args) exprl)
+      else CAppExpl ((qid, us), List.map (add_args id new_args) exprl)
+    | CApp (b, bl) ->
       CApp
-        ( (pf, add_args id new_args b)
+        ( add_args id new_args b
         , List.map (fun (e, o) -> (add_args id new_args e, o)) bl )
+    | CProj (expl, f, bl, b) ->
+      CProj
+        (expl, f
+        , List.map (fun (e, o) -> (add_args id new_args e, o)) bl
+        , add_args id new_args b)
     | CCases (sty, b_option, cel, cal) ->
       CCases
         ( sty
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5bfb37f4cbea..2c628e568068 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -553,7 +553,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       in
       build_entry_lc env sigma funnames avoid
         (mkGLetIn (new_n, v, t, mkGApp (new_b, args)))
-    | GCases _ | GIf _ | GLetTuple _ ->
+    | GCases _ | GIf _ | GLetTuple _ | GProj _ ->
       (* we have [(match e1, ...., en with ..... end) t1 tn]
          we first compute the result from the case and
          then combine each of them with each of args one
@@ -573,6 +573,23 @@ let rec build_entry_lc env sigma funnames avoid rt :
     | GFloat _ -> user_err Pp.(str "Cannot apply a float")
     | GArray _ -> user_err Pp.(str "Cannot apply an array")
     (* end of the application treatement *) )
+  | GProj (f, params, c) ->
+    let args_res : glob_constr list build_entry_return =
+      List.fold_right
+        (* create the arguments lists of constructors and combine them *)
+          (fun arg ctxt_argsl ->
+          let arg_res =
+            build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
+          in
+          combine_results combine_args arg_res ctxt_argsl)
+        (params@[c]) (mk_result [] [] avoid) in
+      { args_res with
+        result =
+          List.map
+            (fun args_res ->
+              let c, params = List.sep_last args_res.value in
+              {args_res with value = DAst.make (GProj (f, params, c))})
+            args_res.result }
   | GLambda (n, _, t, b) ->
     (* we first compute the list of constructor
        corresponding to the body of the function,
@@ -1182,6 +1199,8 @@ let rec compute_cst_params relnames params gt =
         | GVar relname' when Id.Set.mem relname' relnames ->
           compute_cst_params_from_app [] (params, args)
         | _ -> List.fold_left (compute_cst_params relnames) params (f :: args) )
+      | GProj (f, args, c) ->
+        List.fold_left (compute_cst_params relnames) params (args @ [c])
       | GLambda (_, _, t, b) | GProd (_, _, t, b) | GLetTuple (_, _, t, b) ->
         let t_params = compute_cst_params relnames params t in
         compute_cst_params relnames t_params b
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index fb00d2f20296..91dd2d0e697f 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -64,6 +64,8 @@ let change_vars =
           GVar new_id | GEvar _ as x -> x | GPatVar _ as x -> x
         | GApp (rt', rtl) ->
           GApp (change_vars mapping rt', List.map (change_vars mapping) rtl)
+        | GProj (f, rtl, rt) ->
+          GProj (f, List.map (change_vars mapping) rtl, change_vars mapping rt)
         | GLambda (name, k, t, b) ->
           GLambda
             ( name
@@ -288,6 +290,8 @@ let rec alpha_rt excluded rt =
       GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c)
     | GApp (f, args) ->
       GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args)
+    | GProj (f, args, c) ->
+      GProj (f, List.map (alpha_rt excluded) args, alpha_rt excluded c)
     | GArray (u, t, def, ty) ->
       GArray
         ( u
@@ -313,7 +317,7 @@ let is_free_in id =
     DAst.with_loc_val
       (fun ?loc -> function GRef _ -> false | GVar id' -> Id.compare id' id == 0
         | GEvar _ -> false | GPatVar _ -> false
-        | GApp (rt, rtl) -> List.exists is_free_in (rt :: rtl)
+        | GApp (rt, rtl) | GProj (_, rtl, rt) -> List.exists is_free_in (rt :: rtl)
         | GLambda (n, _, t, b) | GProd (n, _, t, b) ->
           let check_in_b =
             match n with Name id' -> not (Id.equal id' id) | _ -> true
@@ -378,6 +382,8 @@ let replace_var_by_term x_id term =
         | (GRef _ | GVar _ | GEvar _ | GPatVar _) as rt -> rt
         | GApp (rt', rtl) ->
           GApp (replace_var_by_pattern rt', List.map replace_var_by_pattern rtl)
+        | GProj (f, rtl, rt) ->
+          GProj (f, List.map replace_var_by_pattern rtl, replace_var_by_pattern rt)
         | GLambda (Name id, _, _, _) as rt when Id.compare id x_id == 0 -> rt
         | GLambda (name, k, t, b) ->
           GLambda (name, k, replace_var_by_pattern t, replace_var_by_pattern b)
@@ -506,6 +512,7 @@ let expand_as =
       | GVar id as rt -> (
         try DAst.get (Id.Map.find id map) with Not_found -> rt )
       | GApp (f, args) -> GApp (expand_as map f, List.map (expand_as map) args)
+      | GProj (f, args, c) -> GProj (f, List.map (expand_as map) args, expand_as map c)
       | GLambda (na, k, t, b) ->
         GLambda (na, k, expand_as map t, expand_as map b)
       | GProd (na, k, t, b) -> GProd (na, k, expand_as map t, expand_as map b)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a907813752d9..a6102a9a7f0a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1757,11 +1757,11 @@ let rec strategy_of_ast ist = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((qualid_of_ident (Id.of_string s),None),l)
 
 let declare_an_instance n s args =
   (((CAst.make @@ Name n),None),
-   CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args))
+   CAst.make @@ CAppExpl ((qualid_of_string s,None), args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
@@ -1978,7 +1978,7 @@ let add_morphism atts binders m s n =
   let instance_name = (CAst.make @@ Name instance_id),None in
   let instance_t =
     CAst.make @@ CAppExpl
-      ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
+      ((Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 843570f6e970..98cd26344f55 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -406,7 +406,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
-  | Inr { v = CAppExpl((None,r,None),[]) } ->
+  | Inr { v = CAppExpl((r,None),[]) } ->
       (* We interpret similarly @ref and ref *)
       interp_ref (make @@ AN r)
   | Inr c ->
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 90e22d4ffe60..9e4529796ce1 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -193,10 +193,10 @@ END
 {
 
 let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
-  | { v = CAppExpl ((None, r,x), args) } when isCHoles args ->
+  | { v = CAppExpl ((r,x), args) } when isCHoles args ->
     prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
-  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc env sigma c
-  | { v = CApp ((_, c), args) } when isCxHoles args ->
+  | { v = CApp ({ v = CRef _ }, _) } as c -> prc env sigma c
+  | { v = CApp (c, args) } when isCxHoles args ->
     prc env sigma c ++ str "|" ++ int (List.length args)
   | c -> prc env sigma c
 
@@ -211,7 +211,7 @@ let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c
 let pr_ssrhintref env sigma prc _ _ = prc env sigma
 
 let mkhintref ?loc c n = match c.CAst.v with
-  | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n)
+  | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((r, x), mkCHoles ?loc n)
   | _ -> mkAppC (c, mkCHoles ?loc n)
 
 }
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 482b47b00734..49166a68e388 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -940,7 +940,7 @@ let id_of_cpattern {pattern = (c1, c2); _} =
   match DAst.get c1, c2 with
   | _, Some { v = CRef (qid, _) } when qualid_is_ident qid ->
     Some (qualid_basename qid)
-  | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid ->
+  | _, Some { v = CAppExpl ((qid, _), []) } when qualid_is_ident qid ->
     Some (qualid_basename qid)
   | GRef (GlobRef.VarRef x, _), None -> Some x
   | _ -> None
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 48f34e7c6b28..4825a9adc7e4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1072,6 +1072,15 @@ let rec subst_glob_constr env subst = DAst.map (function
         if r' == r && rl' == rl then raw else
           GApp(r',rl')
 
+  | GProj ((cst,u),rl,r) as raw ->
+      let rl' = List.Smart.map (subst_glob_constr env subst) rl
+      and r' = subst_glob_constr env subst r in
+      let ref = GlobRef.ConstRef cst in
+      let ref',t = subst_global subst ref in
+      assert (t = None); (* projection *)
+        if ref' == ref && rl' == rl && r' == r then raw else
+          GProj((destConstRef ref',u),rl',r')
+
   | GLambda (n,bk,r1,r2) as raw ->
       let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
         if r1' == r1 && r2' == r2 then raw else
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5a8ac32ffa61..21379d477894 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -171,13 +171,17 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
+  | GProj ((cst1, u1), args1, c1), GProj ((cst2, u2), args2, c2) ->
+    GlobRef.(equal (ConstRef cst1) (ConstRef cst2)) &&
+    Option.equal (List.equal glob_level_eq) u1 u2 &&
+    List.equal f args1 args2 && f c1 c2
   | GInt i1, GInt i2 -> Uint63.equal i1 i2
   | GFloat f1, GFloat f2 -> Float64.equal f1 f2
   | GArray (u1, t1, def1, ty1), GArray (u2, t2, def2, ty2) ->
     Array.equal f t1 t2 && f def1 def2 && f ty1 ty2 &&
     Option.equal (List.equal glob_level_eq) u1 u2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
-     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ |
+     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _ |
      GInt _ | GFloat _ | GArray _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
@@ -237,6 +241,10 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
+  | GProj (p,args,c) ->
+      let comp1 = Util.List.map_left f args in
+      let comp2 = f c in
+      GProj (p,comp1,comp2)
   | GArray (u,t,def,ty) ->
       let comp1 = Array.map_left f t in
       let comp2 = f def in
@@ -274,6 +282,8 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t in
     f acc c
+  | GProj (p,args,c) ->
+    f (List.fold_left f acc args) c
   | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc
   )
@@ -317,6 +327,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t in
     f v acc c
+  | GProj (p,args,c) ->
+    f v (List.fold_left (f v) acc args) c
   | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc))
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index d480c1283443..fe3ad26993b4 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -95,6 +95,7 @@ type 'a glob_constr_r =
   | GSort of glob_sort
   | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+  | GProj of (Constant.t * glob_level list option) * 'a glob_constr_g list * 'a glob_constr_g
   | GInt of Uint63.t
   | GFloat of Float64.t
   | GArray of glob_level list option * 'a glob_constr_g array * 'a glob_constr_g * 'a glob_constr_g
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0c4bbf71e2f7..51d2e6f120dc 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -432,6 +432,13 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PApp (pat_of_raw metas vars c,
             Array.of_list (List.map (pat_of_raw metas vars) cl))
     end
+  | GProj ((p,_), cl, c) ->
+    if Structures.PrimitiveProjections.mem p then
+      let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
+      let p = Projection.make p false in
+      PProj (p, pat_of_raw metas vars c)
+    else
+      PApp (PRef (GlobRef.ConstRef p), Array.map_of_list (pat_of_raw metas vars) (cl @ [c]))
   | GLambda (na,bk,c1,c2) ->
       Name.iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9ef62db1027e..e1d1545dce7d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -490,6 +490,7 @@ type pretyper = {
   pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
   pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
   pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
+  pretype_proj : pretyper -> (Constant.t * glob_level list option) * glob_constr list * glob_constr -> unsafe_judgment pretype_fun;
   pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_prod : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_letin : pretyper -> Name.t * glob_constr * glob_constr option * glob_constr -> unsafe_judgment pretype_fun;
@@ -520,6 +521,8 @@ let eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t =
     self.pretype_patvar self knd ?loc ~program_mode ~poly resolve_tc tycon env sigma
   | GApp (c, args) ->
     self.pretype_app self (c, args) ?loc ~program_mode ~poly resolve_tc tycon env sigma
+  | GProj (hd, args, c) ->
+    self.pretype_proj self (hd, args, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma
   | GLambda (na, bk, t, c) ->
     self.pretype_lambda self (na, bk, t, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma
   | GProd (na, bk, t, c) ->
@@ -909,6 +912,11 @@ struct
     in
     (sigma, resj)
 
+  let pretype_proj self ((f,us), args, c) =
+    fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
+    pretype_app self (DAst.make ?loc (GRef (GlobRef.ConstRef f,us)), args @ [c])
+      ?loc ~program_mode ~poly resolve_tc tycon env sigma
+
   let pretype_lambda self (name, bk, c1, c2) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
     let open Context.Rel.Declaration in
@@ -1327,6 +1335,7 @@ let default_pretyper =
     pretype_evar = pretype_evar;
     pretype_patvar = pretype_patvar;
     pretype_app = pretype_app;
+    pretype_proj = pretype_proj;
     pretype_lambda = pretype_lambda;
     pretype_prod = pretype_prod;
     pretype_letin = pretype_letin;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5668098fe6dc..a15ce2644dd7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -150,6 +150,7 @@ type pretyper = {
   pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun;
   pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun;
   pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun;
+  pretype_proj : pretyper -> (Constant.t * glob_level list option) * glob_constr list * glob_constr -> unsafe_judgment pretype_fun;
   pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_prod : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun;
   pretype_letin : pretyper -> Name.t * glob_constr * glob_constr option * glob_constr -> unsafe_judgment pretype_fun;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d7d9382bdb95..8da664296537 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -571,36 +571,21 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CAppExpl ((Some i,f,us),l) ->
-        let l1,l2 = List.chop i l in
-        let c,l1 = List.sep_last l1 in
-        let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
-        if not (List.is_empty l2) then
-          return (hov 0 (p ++ prlist (pr spc (LevelLt lapp)) l2), lapp)
-        else
-          return (p, lproj)
-      | CAppExpl ((None,qid,us),[t])
-      | CApp ((_, {v = CRef(qid,us)}),[t,None])
+      | CProj (true,(f,us),l,c) ->
+        let l = List.map (function (c,None) -> c | _ -> assert false) l in
+        return (pr_proj (pr mt) pr_appexpl c (f,us) l, lproj)
+      | CProj (false,(f,us),l,c) ->
+        return (pr_proj (pr mt) pr_app c (CAst.make (CRef (f,us))) l, lproj)
+      | CAppExpl ((qid,us),[t])
+      | CApp ({v = CRef(qid,us)},[t,None])
           when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
         return (
           hov 0 (str ".." ++ pr spc (LevelLe latom) t ++ spc () ++ str ".."),
           larg
         )
-      | CAppExpl ((None,f,us),l) ->
+      | CAppExpl ((f,us),l) ->
         return (pr_appexpl (pr mt) (f,us) l, lapp)
-      | CApp ((Some i,f),l) ->
-        let l1,l2 = List.chop i l in
-        let c,l1 = List.sep_last l1 in
-        assert (Option.is_empty (snd c));
-        let p = pr_proj (pr mt) pr_app (fst c) f l1 in
-        if not (List.is_empty l2) then
-          return (
-            hov 0 (p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2),
-            lapp
-          )
-        else
-          return (p, lproj)
-      | CApp ((None,a),l) ->
+      | CApp (a,l) ->
         return (pr_app (pr mt) a l, lapp)
       | CRecord l ->
         return (pr_record_body "{|" "|}" (pr spc ltop) l, latom)
@@ -712,7 +697,7 @@ let tag_var = tag Tag.variable
        that we cannot use [pr] correctly anymore in a recursive loop
        if the current expr is followed by other exprs which would be
        interpreted as arguments *)
-    | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
+    | { CAst.v = CAppExpl ((f,us),[]) } -> str "@" ++ pr_cref f us
     | c -> pr prec c
 
   let transf env sigma c =
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index eb576d4347a9..a4f0356fef4f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -500,12 +500,16 @@ let match_goals ot nt =
       constr_expr ogname c1 c12;
       constr_expr_opt ogname t t2;
       constr_expr ogname c2 c22
-    | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) ->
+    | CAppExpl ((ref,us),args), CAppExpl ((ref2,us2),args2) ->
       iter2 (constr_expr ogname) args args2
-    | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) ->
+    | CApp (f,args), CApp (f2,args2) ->
       constr_expr ogname f f2;
       iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
           constr_expr ogname c c2) args args2
+    | CProj (expl,f,args,c), CProj (expl2,f2,args2,c2) ->
+      iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
+          constr_expr ogname c c2) args args2;
+      constr_expr ogname c c2;
     | CRecord fs, CRecord fs2 ->
       iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in
           constr_expr ogname c c2) fs fs2
diff --git a/test-suite/output/bug_6764.out b/test-suite/output/bug_6764.out
new file mode 100644
index 000000000000..2e07f14d8fba
--- /dev/null
+++ b/test-suite/output/bug_6764.out
@@ -0,0 +1,8 @@
+forall f : foo, ■ f = ■ f
+     : Prop
+forall f : foo, ■ f = ■ f
+     : Prop
+fun x : T => %% x
+     : T -> nat
+fun x : T => %% x
+     : T -> nat
diff --git a/test-suite/output/bug_6764.v b/test-suite/output/bug_6764.v
new file mode 100644
index 000000000000..9197b66ea43d
--- /dev/null
+++ b/test-suite/output/bug_6764.v
@@ -0,0 +1,27 @@
+Module A.
+Set Primitive Projections.
+Record foo := Foo { foo_n : nat }.
+Notation "'■' x" := (foo_n x) (at level 50).
+Check forall (f:foo), ■ f = ■ f.
+End A.
+
+Module A'.
+Set Primitive Projections.
+Record foo := Foo { foo_n : nat }.
+Notation "'■' x" := x.(foo_n) (at level 50).
+Check forall (f:foo), ■ f = ■ f.
+End A'.
+
+(* Variant with non-primitive projections *)
+
+Module B.
+Record T := {a:nat}.
+Notation "%% x" := (a x) (at level 0, x at level 0).
+Check fun x => %%x.
+End B.
+
+Module B'.
+Record T := {a:nat}.
+Notation "%% x" := x.(a) (at level 0, x at level 0).
+Check fun x => %%x.
+End B'.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index e371cf251f1f..c3615e8eccd0 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -504,10 +504,22 @@ reflexivity.
 simpl;rewrite IHn0;reflexivity.
 Qed.
 
+(* An example with projections *)
 
+Require Import FunInd.
+Require Import List.
 
+Record foo (X:Type):= {a:nat; b:X}.
 
+Inductive ind X: Type :=
+| C: foo X -> ind X
+| D: ind X -> ind X.
 
-
-
-
+Function f X (deflt:X) (x:ind X) {struct x} :=
+  match x with
+    @C _ fo => match fo.(a X) with
+             O => fo.(b X)
+           | S n => deflt
+           end
+  | D _ d => f _ deflt d
+  end.