Merge PR #13265: Add support for general non-necessarily-recursive binders in notations

Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle

24 files changed, 362 insertions, 193 deletions

diff --git a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst
new file mode 100644
index 0000000000..c973e157dd
--- /dev/null
+++ b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  The :n:`@binder` entry of :cmd:`Notation` can now be used in
+  notations expecting a single (non-recursive) binder
+  (`#13265 <https://github.com/coq/coq/pull/13265>`_,
+  by Hugo Herbelin, see section :n:`notations-and-binders` of the
+  reference manual).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 16c8586a9f..5cbd2e400e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -709,6 +709,30 @@ Note also that in the absence of a ``as ident``, ``as strict pattern`` or
 ``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring
 in binding position and parsed as terms to be ``as ident``.
 
+Binders bound in the notation and parsed as general binders
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+It is also possible to rely on Coq's syntax of binders using the
+`binder` modifier as follows:
+
+.. coqtop:: in
+
+   Notation "'myforall' p , [ P , Q ] " := (forall p, P -> Q)
+     (at level 200, p binder).
+
+In this case, all of :n:`@ident`, :n:`{@ident}`, :n:`[@ident]`, :n:`@ident:@type`,
+:n:`{@ident:@type}`, :n:`[@ident:@type]`, :n:`'@pattern` can be used in place of
+the corresponding notation variable. In particular, the binder can
+declare implicit arguments:
+
+.. coqtop:: all
+
+   Check fun (f : myforall {a}, [a=0, Prop]) => f eq_refl.
+   Check myforall '((x,y):nat*nat), [ x = y, True ].
+
+By using instead `closed binder`, the same list of binders is allowed
+except that :n:`@ident:@type` requires parentheses around.
+
 .. _NotationsWithBinders:
 
 Binders not bound in the notation
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 977cbbccf2..b3f06faa1c 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -83,6 +83,8 @@ type cases_pattern_expr_r =
   | CPatCast   of cases_pattern_expr * constr_expr
 and cases_pattern_expr = cases_pattern_expr_r CAst.t
 
+and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
+
 and cases_pattern_notation_substitution =
     cases_pattern_expr list *     (* for constr subterms *)
     cases_pattern_expr list list  (* for recursive notations *)
@@ -145,12 +147,12 @@ and recursion_order_expr = recursion_order_expr_r CAst.t
 and local_binder_expr =
   | CLocalAssum   of lname list * binder_kind * constr_expr
   | CLocalDef     of lname * constr_expr * constr_expr option
-  | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+  | CLocalPattern of cases_pattern_expr
 
 and constr_notation_substitution =
     constr_expr list *      (* for constr subterms *)
     constr_expr list list * (* for recursive notations *)
-    cases_pattern_expr list *   (* for binders *)
+    kinded_cases_pattern_expr list *   (* for binders *)
     local_binder_expr list list (* for binder lists (recursive notations) *)
 
 type constr_pattern_expr = constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index efc2a35b65..a60dc11b57 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -94,6 +94,9 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
   List.equal cases_pattern_expr_eq s1 s2 &&
   List.equal (List.equal cases_pattern_expr_eq) n1 n2
 
+let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) =
+  cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2
+
 let eq_universes u1 u2 =
   match u1, u2 with
   | None, None -> true
@@ -231,7 +234,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
 and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
   List.equal constr_expr_eq e1 e2 &&
   List.equal (List.equal constr_expr_eq) el1 el2 &&
-  List.equal cases_pattern_expr_eq b1 b2 &&
+  List.equal kinded_cases_pattern_expr_eq b1 b2 &&
   List.equal (List.equal local_binder_eq) bl1 bl2
 
 and instance_eq (x1,c1) (x2,c2) =
@@ -268,39 +271,37 @@ let is_constructor id =
            (Nametab.locate_extended (qualid_of_ident id)))
   with Not_found -> false
 
-let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
+let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
   | CPatRecord l ->
-    List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
-  | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
+    List.fold_left (fun nacc (r, cp) -> cases_pattern_fold_names f h nacc cp) nacc l
+  | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right (fun na (n,acc) -> (f na n,acc)) na (cases_pattern_fold_names f h nacc pat)
   | CPatOr (patl) ->
-    List.fold_left (cases_pattern_fold_names f) a patl
+    List.fold_left (cases_pattern_fold_names f h) nacc patl
   | CPatCstr (_,patl1,patl2) ->
-    List.fold_left (cases_pattern_fold_names f)
-      (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
+    List.fold_left (cases_pattern_fold_names f h)
+      (Option.fold_left (List.fold_left (cases_pattern_fold_names f h)) nacc patl1) patl2
   | CPatNotation (_,_,(patl,patll),patl') ->
-    List.fold_left (cases_pattern_fold_names f)
-      (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
-  | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
+    List.fold_left (cases_pattern_fold_names f h)
+      (List.fold_left (cases_pattern_fold_names f h) nacc (patl@List.flatten patll)) patl'
+  | CPatDelimiters (_,pat) -> cases_pattern_fold_names f h nacc pat
   | CPatAtom (Some qid)
       when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
-      f (qualid_basename qid) a
-  | CPatPrim _ | CPatAtom _ -> a
-  | CPatCast ({CAst.loc},_) ->
-    CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
-      (Pp.strbrk "Casts are not supported here.")
-
-let ids_of_pattern =
-  cases_pattern_fold_names Id.Set.add Id.Set.empty
-
-let ids_of_pattern_list =
-  List.fold_left
-    (List.fold_left (cases_pattern_fold_names Id.Set.add))
-    Id.Set.empty
+      let (n, acc) = nacc in
+      (f (qualid_basename qid) n, acc)
+  | CPatPrim _ | CPatAtom _ -> nacc
+  | CPatCast (p,t) ->
+      let (n, acc) = nacc in
+      cases_pattern_fold_names f h (n, h acc t) p
+
+let ids_of_pattern_list p =
+  fst (List.fold_left
+    (List.fold_left (cases_pattern_fold_names Id.Set.add (fun () _ -> ())))
+    (Id.Set.empty,()) p)
 
 let ids_of_cases_tomatch tms =
   List.fold_right
     (fun (_, ona, indnal) l ->
-       Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+       Option.fold_right (fun t ids -> fst (cases_pattern_fold_names Id.Set.add (fun () _ -> ()) (ids,()) t))
          indnal
          (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
@@ -312,9 +313,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function
     f n (fold_local_binders g f n' acc b l) t
   | CLocalDef ( { v = na },c,t)::l ->
     Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
-  | CLocalPattern { v = pat,t }::l ->
-    let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
-    Option.fold_left (f n) acc t
+  | CLocalPattern pat :: l ->
+    let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
+    fold_local_binders g f n acc b l
   | [] ->
     f n acc b
 
@@ -378,10 +379,42 @@ let names_of_constr_expr c =
 
 let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 
+let rec fold_map_cases_pattern f h acc (CAst.{v=pt;loc} as p) = match pt with
+  | CPatRecord l ->
+    let acc, l = List.fold_left_map (fun acc (r, cp) -> let acc, cp = fold_map_cases_pattern f h acc cp in acc, (r, cp)) acc l in
+    acc, CAst.make ?loc (CPatRecord l)
+  | CPatAlias (pat,({CAst.v=na} as lna)) ->
+    let acc, p = fold_map_cases_pattern f h acc pat in
+    let acc = Name.fold_right f na acc in
+    acc, CAst.make ?loc (CPatAlias (pat,lna))
+  | CPatOr patl ->
+    let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+    acc, CAst.make ?loc (CPatOr patl)
+  | CPatCstr (c,patl1,patl2) ->
+    let acc, patl1 = Option.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patl1 in
+    let acc, patl2 = List.fold_left_map (fold_map_cases_pattern f h) acc patl2 in
+    acc, CAst.make ?loc (CPatCstr (c,patl1,patl2))
+  | CPatNotation (sc,ntn,(patl,patll),patl') ->
+    let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+    let acc, patll = List.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patll in
+    let acc, patl' = List.fold_left_map (fold_map_cases_pattern f h) acc patl' in
+    acc, CAst.make ?loc (CPatNotation (sc,ntn,(patl,patll),patl'))
+  | CPatDelimiters (d,pat) ->
+    let acc, p = fold_map_cases_pattern f h acc pat in
+    acc, CAst.make ?loc (CPatDelimiters (d,pat))
+  | CPatAtom (Some qid)
+      when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+    f (qualid_basename qid) acc, p
+  | CPatPrim _ | CPatAtom _ -> (acc,p)
+  | CPatCast (pat,t) ->
+    let acc, pat = fold_map_cases_pattern f h acc pat in
+    let t = h acc t in
+    acc, CAst.make ?loc (CPatCast (pat,t))
+
 (* Used in correctness and interface *)
 let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
 
-let map_local_binders f g e bl =
+let fold_map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let open CAst in
   let h (e,bl) = function
@@ -389,9 +422,9 @@ let map_local_binders f g e bl =
       (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
     | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
       (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
-    | CLocalPattern { loc; v = pat,t } ->
-      let ids = ids_of_pattern pat in
-      (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
+    | CLocalPattern pat ->
+      let e, pat = fold_map_cases_pattern g f e pat in
+      (e, CLocalPattern pat::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
@@ -400,16 +433,16 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CApp ((p,a),l) ->
       CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
     | CProdN (bl,b) ->
-      let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
+      let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
-      let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
+      let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
       CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
     | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
     | CNotation (inscope,n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
       CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
-                    List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
+                    List.map (fun bl -> snd (fold_map_local_binders f g e bl)) bll))
     | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
     | CDelimiters (s,a) -> CDelimiters (s,f e a)
     | CHole _ | CEvar _ | CPatVar _ | CSort _
@@ -431,7 +464,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
     | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->
-          let (e',bl') = map_local_binders f g e bl in
+          let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
           (* Note: fix names should be inserted before the arguments... *)
           let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
@@ -439,7 +472,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
           (id,n,bl',t',d')) dl)
     | CCoFix (id,dl) ->
       CCoFix (id,List.map (fun (id,bl,t,d) ->
-          let (e',bl') = map_local_binders f g e bl in
+          let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
           let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
@@ -472,7 +505,7 @@ let locs_of_notation ?loc locs ntn =
 let ntn_loc ?loc (args,argslist,binders,binderslist) =
   locs_of_notation ?loc
     (List.map constr_loc (args@List.flatten argslist)@
-     List.map cases_pattern_expr_loc binders@
+     List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@
      List.map local_binders_loc binderslist)
 
 let patntn_loc ?loc (args,argslist) =
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8d3cf7274a..cf88036f73 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1126,7 +1126,7 @@ and factorize_prod ?impargs scopes vars na bk t c =
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = extern_typ scopes vars b in
       let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
-      let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+      let binder = CLocalPattern p in
       (match b.v with
       | CProdN (bl,b) -> CProdN (binder::bl,b)
       | _ -> CProdN ([binder],b))
@@ -1167,7 +1167,7 @@ and factorize_lambda inctx scopes vars na bk t c =
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = sub_extern inctx scopes vars b in
       let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
-      let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+      let binder = CLocalPattern p in
       (match b.v with
       | CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
       | _ -> CLambdaN ([binder],b))
@@ -1219,7 +1219,10 @@ and extern_local_binder scopes vars = function
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
+      let p = match ty with
+        | None -> p
+        | Some ty -> CAst.make @@ (CPatCast (p,ty)) in
+      (assums,ids, CLocalPattern p :: l)
 
 and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
@@ -1303,7 +1306,8 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
                       termlists in
                   let bl =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
-                      mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
+                      (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)),
+                      Explicit)
                       binders in
                   let bll =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c7ed066f7e..8bd77abc4a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -298,21 +298,20 @@ let error_expect_binder_notation_type ?loc id =
 let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
   try
     let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
-    if not istermvar then used_as_binder := true;
-    let () = if istermvar then
+    if istermvar then begin
       (* scopes have no effect on the interpretation of identifiers *)
-      begin match !idscopes with
+      (match !idscopes with
       | None -> idscopes := Some scopes
       | Some (tmp_scope', subscopes') ->
         let s' = make_current_scope tmp_scope' subscopes' in
         let s = make_current_scope tmp_scope subscopes in
-        if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s
+        if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s);
+      (match typ with
+      | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
+      | Notation_term.NtnInternTypeAny -> ())
       end
-    in
-    match typ with
-    | Notation_term.NtnInternTypeOnlyBinder ->
-        if istermvar then error_expect_binder_notation_type ?loc id
-    | Notation_term.NtnInternTypeAny -> ()
+    else
+      used_as_binder := true
   with Not_found ->
     (* Not in a notation *)
     ()
@@ -587,7 +586,10 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
   (push_name_env ntnvars impls env locna,
    (na,Explicit,term,ty))
 
-let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
+let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) =
+  let p,t = match p with
+  | CPatCast (p, t) -> (p, Some t)
+  | _ -> (pv, None) in
   let il,disjpat =
     let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in
     let substl,disjpat = List.split subst_disjpat in
@@ -595,12 +597,17 @@ let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
       user_err ?loc (str "Unsupported nested \"as\" clause.");
     il,disjpat
   in
-  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
   let na = alias_of_pat (List.hd disjpat) in
+  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
   let ienv = Name.fold_right Id.Set.remove na env.ids in
   let id = Namegen.next_name_away_with_default "pat" na ienv in
   let na = make ?loc @@ Name id in
-  env,((disjpat,il),id),na
+  let t = match t with
+    | Some t -> t
+    | None -> CAst.make ?loc @@ CHole(Some (Evar_kinds.BinderType na.v),IntroAnonymous,None) in
+  let _, bl' = intern_assumption intern ntnvars env [na] (Default bk) t in
+  let {v=(_,bk,t)} = List.hd bl' in
+  env,((disjpat,il),id),na,bk,t
 
 let intern_local_binder_aux intern ntnvars (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
@@ -610,17 +617,9 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function
   | CLocalDef( {loc; v=na} as locna,def,ty) ->
      let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
      env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl
-  | CLocalPattern {loc;v=(p,ty)} ->
-      let tyc =
-        match ty with
-        | Some ty -> ty
-        | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
-      in
-      let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in
-      let bk = Default Explicit in
-      let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
-      let {v=(_,bk,t)} = List.hd bl' in
-      (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
+  | CLocalPattern p ->
+      let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in
+      (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
 
 let intern_generalization intern env ntnvars loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -706,7 +705,7 @@ let is_patvar c =
 
 let is_patvar_store store pat =
   match DAst.get pat with
-  | PatVar na -> ignore(store na); true
+  | PatVar na -> ignore(store (CAst.make ?loc:pat.loc na)); true
   | _ -> false
 
 let out_patvar = CAst.map_with_loc (fun ?loc -> function
@@ -715,37 +714,57 @@ let out_patvar = CAst.map_with_loc (fun ?loc -> function
   | CPatAtom None -> Anonymous
   | _ -> assert false)
 
-let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env), None, Anonymous
+let canonize_type = function
+  | None -> None
+  | Some t as t' ->
+    match DAst.get t with
+    | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+    | _ -> t'
+
+let set_type ty1 ty2 =
+  match canonize_type ty1, canonize_type ty2 with
+  (* Not a meta-binding binder, we use the type given in the notation *)
+  | _, None -> ty1
+  (* A meta-binding binder meta-bound to a possibly-typed pattern *)
+  (* the binder is supposed to come w/o an explicit type in the notation *)
+  | None, Some _ -> ty2
+  | Some ty1, Some t2 ->
+    (* An explicitly typed meta-binding binder, not supposed to be a pattern; checked in interp_notation *)
+    user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.")
+
+let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty =
+ match na with
+ | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
  | Name id ->
   let store,get = set_temporary_memory () in
   let test_kind = test_kind_tolerant in
   try
     (* We instantiate binder name with patterns which may be parsed as terms *)
     let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
-    let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
+    let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env Explicit pat in
     let pat, na = match disjpat with
     | [pat] when is_patvar_store store pat -> let na = get () in None, na
-    | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
-    (renaming,env), pat, na
+    | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+    (renaming,env), pat, na.v, bk, set_type ty (Some t)
   with Not_found ->
   try
     (* Trying to associate a pattern *)
-    let pat,(onlyident,scopes) = Id.Map.find id binders in
+    let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
     let env = set_env_scopes env scopes in
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_patvar pat in
       let env = push_name_env ntnvars [] env na in
-      (renaming,env), None, na.v
+      let ty' = DAst.make @@ GHole (Evar_kinds.BinderType na.CAst.v,IntroAnonymous,None) in
+      (renaming,env), None, na.v, bk, set_type ty (Some ty')
     else
       (* Interpret as a pattern *)
-      let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
+      let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env bk pat in
       let pat, na =
         match disjpat with
         | [pat] when is_patvar_store store pat -> let na = get () in None, na
-        | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
-      (renaming,env), pat, na
+        | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+      (renaming,env), pat, na.v, bk, set_type ty (Some t)
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -753,7 +772,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let renaming' =
       if Id.equal id id' then renaming else Id.Map.add id id' renaming
     in
-    (renaming',env), None, Name id'
+    (renaming',env), None, Name id', Explicit, set_type ty None
 
 type binder_action =
 | AddLetIn of lname * constr_expr * constr_expr option
@@ -878,12 +897,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
             Id.Map.add id (gc, None) map
           with Nametab.GlobalizationError _ -> map
         in
-        let mk_env' (c, (onlyident,scopes)) =
-          let nenv = set_env_scopes env scopes in
+        let mk_env' ((c,_bk), (onlyident,(tmp_scope,subscopes))) =
+          let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
           let test_kind =
             if onlyident then test_kind_ident_in_notation
             else test_kind_pattern_in_notation in
-          let _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in
+          let _,((disjpat,_),_),_,_,_ty = intern_pat test_kind ntnvars nenv Explicit c in
+          (* TODO: use cast? *)
           match disjpat with
           | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
           | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
@@ -908,26 +928,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
         aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
       with Not_found ->
           anomaly (Pp.str "Inconsistent substitution of recursive notation."))
-    | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
+    | NProd (Name id, None, c') when option_mem_assoc id binderopt ->
         let binder = snd (Option.get binderopt) in
         expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c')
-    | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
+    | NLambda (Name id, None, c') when option_mem_assoc id binderopt ->
         let binder = snd (Option.get binderopt) in
         expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c')
-    (* Two special cases to keep binder name synchronous with BinderType *)
-    | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
-        when Name.equal na na' ->
-        let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
-        let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-        DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
-    | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
-        when Name.equal na na' ->
-        let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst  avoid subinfos na in
-        let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-        DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
     | t ->
       glob_constr_of_notation_constr_with_binders ?loc
-        (traverse_binder intern_pat ntnvars subst  avoid) (aux subst') ~h:binder_status_fun subinfos t
+        (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
   and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
@@ -936,12 +945,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       intern (set_env_scopes env scopes) a
     with Not_found ->
     try
-      let pat,(onlyident,scopes) = Id.Map.find id binders in
-      let nenv = set_env_scopes env scopes in
+      let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
+      let env = set_env_scopes env scopes in
       let test_kind =
         if onlyident then test_kind_ident_in_notation
         else test_kind_pattern_in_notation in
-      let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars nenv pat in
+      let env,((disjpat,ids),id),na,bk,_ty = intern_pat test_kind ntnvars env bk pat in
+      (* TODO: use cast? *)
       match disjpat with
       | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
       | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
@@ -983,13 +993,13 @@ let split_by_type ids subst =
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
-       let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
+       let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
-       let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
+       let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
        let onlyident = (x = NtnParsedAsIdent) in
        let binders,binders' = bind id (onlyident,scl) binders binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
@@ -1031,7 +1041,7 @@ let intern_notation intern env ntnvars loc ntn fullargs =
   (* Dispatch parsing substitution to an interpretation substitution *)
   let subst = split_by_type ids fullargs in
   (* Instantiate the notation *)
-  instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst (Id.Map.empty, env) c
+  instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst (Id.Map.empty, env) c
 
 (**********************************************************************)
 (* Discriminating between bound variables and global references       *)
@@ -1159,7 +1169,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       check_no_explicitation args1;
       let subst = split_by_type ids (List.map fst args1,[],[],[]) in
       let infos = (Id.Map.empty, env) in
-      let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
+      let c = instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst infos c in
       let loc = c.loc in
       let err () =
         user_err ?loc  (str "Notation " ++ pr_qualid qid
diff --git a/interp/notation.ml b/interp/notation.ml
index 286ece6cb6..b5951a9c59 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -64,7 +64,8 @@ let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+| NtnParsedAsBinder,  NtnParsedAsBinder -> true
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c4d2a2a496..f51d3bfdfb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -131,7 +131,11 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
   | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
   | NLambda (na1, t1, u1), NLambda (na2, t2, u2)
   | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
-    aux vars renaming t1 t2;
+    (match t1, t2 with
+     | None, None -> ()
+     | Some _, None -> if lt then strictly_lt := true
+     | Some t1, Some t2 -> aux vars renaming t1 t2
+     | None, Some _ -> raise Exit);
     let renaming = check_eq_name vars renaming na1 na2 in
     aux vars renaming u1 u2
   | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
@@ -272,11 +276,25 @@ let default_binder_status_fun = {
   slide = (fun x -> x);
 }
 
+let test_implicit_argument_mark bk =
+  if not (Glob_ops.binding_kind_eq bk Explicit) then
+    user_err (Pp.str "Unexpected implicit argument mark.")
+
+let test_pattern_cast = function
+  | None -> ()
+  | Some t -> user_err ?loc:t.CAst.loc (Pp.str "Unsupported pattern cast.")
+
 let protect g e na =
-  let e',disjpat,na = g e na in
+  let e',disjpat,na,bk,t = g e na None in
   if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  test_implicit_argument_mark bk;
+  test_pattern_cast t;
   e',na
 
+let set_anonymous_type na = function
+  | None -> DAst.make @@ GHole (Evar_kinds.BinderType na, IntroAnonymous, None)
+  | Some t -> t
+
 let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
   let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
   DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
@@ -302,15 +320,21 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
       DAst.get (subst_glob_vars outerl it)
   | NLambda (na,ty,c) ->
       let e = h.switch_lambda e in
-      let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      let ty = Option.map (f (h.restart_prod e)) ty in
+      let e',disjpat,na',bk,ty = g e na ty in
+      GLambda (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NProd (na,ty,c) ->
       let e = h.switch_prod e in
-      let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      let ty = Option.map (f (h.restart_prod e)) ty in
+      let e',disjpat,na',bk,ty = g e na ty in
+      GProd (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',disjpat,na = g e na in
+      let t = Option.map (f (h.restart_prod e)) t in
+      let e',disjpat,na,bk,t = g e na t in
+      test_implicit_argument_mark bk;
       (match disjpat with
-       | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c)
-       | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
+       | None -> GLetIn (na,f (h.restart_lambda e) b,t,f e' c)
+       | Some (disjpat,_id) -> test_pattern_cast t; DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e = h.no e in
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
@@ -323,7 +347,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
           e',Some (CAst.make ?loc (ind,nal')) in
         let e',na' = protect g e' na in
         (e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in
+      let fold (idl,e) na =
+        let (e,disjpat,na,bk,t) = g e na None in
+        test_implicit_argument_mark bk;
+        test_pattern_cast t;
+        ((Name.cons na idl,e),disjpat,na) in
       let eqnl' = List.map (fun (patl,rhs) ->
         let ((idl,e),patl) =
           List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
@@ -356,7 +384,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id t -> ((),None,id,Explicit,t)) aux () x
   in aux () x
 
 (******************************************************************************)
@@ -551,8 +579,8 @@ 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)
-  | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
-  | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,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)
   | GCases (sty,rtntypopt,tml,eqnl) ->
       let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
@@ -589,6 +617,9 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GEvar _ | GPatVar _ ->
       user_err Pp.(str "Existential variables not allowed in notations.")
   ) x
+  and aux_type t = DAst.with_val (function
+  | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+  | _ -> Some (aux t)) t
   in
   let t = aux a in
   (* Side effect *)
@@ -697,13 +728,13 @@ let rec subst_notation_constr subst bound raw =
           NList (id1,id2,r1',r2',b)
 
   | NLambda (n,r1,r2) ->
-      let r1' = subst_notation_constr subst bound r1
+      let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
       and r2' = subst_notation_constr subst bound r2 in
         if r1' == r1 && r2' == r2 then raw else
           NLambda (n,r1',r2')
 
   | NProd (n,r1,r2) ->
-      let r1' = subst_notation_constr subst bound r1
+      let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
       and r2' = subst_notation_constr subst bound r2 in
         if r1' == r1 && r2' == r2 then raw else
           NProd (n,r1',r2')
@@ -819,7 +850,7 @@ let abstract_return_type_context_glob_constr tml rtn =
 
 let abstract_return_type_context_notation_constr tml rtn =
   abstract_return_type_context snd
-    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
+    (fun na c -> NLambda(na,None,c)) tml rtn
 
 let rec push_pattern_binders vars pat =
   match DAst.get pat with
@@ -852,6 +883,7 @@ let is_onlybinding_pattern_like_meta isvar id metas =
       | _,NtnTypeBinder (NtnBinderParsedAsConstr
                            (AsIdentOrPattern | AsStrictPattern)) -> true
       | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+      | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
       | _ -> false
   with Not_found -> false
 
@@ -1325,9 +1357,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_hd u alp metas sigma f1 f2) l1 l2
   | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) ->
-     match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 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) ->
-     match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2
+     match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
   | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
   | GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
@@ -1396,14 +1428,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
      otherwise how to ensure it corresponds to a well-typed eta-expansion;
      we make an exception for types which are metavariables: this is useful e.g.
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
-  | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+  | _b1, NLambda (Name id as na,(None | Some (NVar _) as t2),b2) when inner ->
       let avoid =
         Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
       let id' = Namegen.next_ident_away id avoid in
       let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in
       let sigma = match t2 with
-      | NHole _ -> sigma
-      | NVar id2 -> bind_term_env alp sigma id2 t1
+      | None -> sigma
+      | Some (NVar id2) -> bind_term_env alp sigma id2 t1
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
@@ -1423,6 +1455,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
      | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
 
+and match_in_type u alp metas sigma t = function
+  | None -> sigma
+  | Some t' -> match_in u alp metas sigma t t'
+
 and match_in u = match_ true u
 
 and match_hd u = match_ false u
@@ -1497,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
           let v = glob_constr_of_cases_pattern (Global.env()) pat in
           (((vars,v),scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 9d451a5bb9..e7a0429b35 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,7 +53,7 @@ val apply_cases_pattern : ?loc:Loc.t ->
   (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr
 
 val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
-  ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
+  ('a -> Name.t -> glob_constr option -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t * Glob_term.binding_kind * glob_constr option) ->
   ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun ->
   'a -> notation_constr -> glob_constr
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 82238b71b7..29db23cc54 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -27,8 +27,8 @@ type 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] *)
-  | NLambda of Name.t * notation_constr * notation_constr
-  | NProd of Name.t * notation_constr * notation_constr
+  | NLambda of Name.t * notation_constr option * notation_constr
+  | NProd of Name.t * notation_constr option * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of Constr.case_style * notation_constr option *
@@ -78,6 +78,8 @@ type notation_binder_source =
   | NtnParsedAsIdent
   (* This accepts ident, or pattern, or both *)
   | NtnBinderParsedAsConstr of constr_as_binder_kind
+  (* This accepts ident, _, and quoted pattern *)
+  | NtnParsedAsBinder
 
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
diff --git a/parsing/extend.ml b/parsing/extend.ml
index a6fa6edad5..94c3768116 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -58,6 +58,7 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
+  | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
   | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 057fdb3841..b698415fd6 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -53,6 +53,7 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
+  | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
   | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 67a061175a..68530178f8 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -39,6 +39,10 @@ let binder_of_name expl { CAst.loc = loc; v = na } =
 let binders_of_names l =
   List.map (binder_of_name Explicit) l
 
+let pat_of_name CAst.{loc;v} = match v with
+| Anonymous -> CAst.make ?loc @@ CPatAtom None
+| Name id -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident id))
+
 let err () = raise Stream.Failure
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
@@ -84,7 +88,8 @@ GRAMMAR EXTEND Gram
   universe_level universe_name sort sort_family
   global constr_pattern cpattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
-  record_declaration typeclass_constraint pattern arg type_cstr;
+  record_declaration typeclass_constraint pattern arg type_cstr
+  one_closed_binder one_open_binder;
   Constr.ident:
     [ [ id = Prim.ident -> { id } ] ]
   ;
@@ -438,13 +443,20 @@ GRAMMAR EXTEND Gram
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
       | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
-      | "'"; p = pattern LEVEL "0" ->
-        { let (p, ty) =
-            match p.CAst.v with
-            | CPatCast (p, ty) -> (p, Some ty)
-            | _ -> (p, None)
-          in
-          [CLocalPattern (CAst.make ~loc (p, ty))] } ] ]
+      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
+  ;
+  one_open_binder:
+    [ [ na = name -> { (pat_of_name na, Explicit) }
+      | na = name; ":"; t = lconstr -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
+      | b = one_closed_binder -> { b } ] ]
+  ;
+  one_closed_binder:
+    [ [ "("; na = name; ":"; t = lconstr; ")" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
+      | "{"; na = name; "}" -> { (pat_of_name na, MaxImplicit) }
+      | "{"; na = name; ":"; t = lconstr; "}" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), MaxImplicit) }
+      | "["; na = name; "]" -> { (pat_of_name na, NonMaxImplicit) }
+      | "["; na = name; ":"; t = lconstr; "]" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), NonMaxImplicit) }
+      | "'"; p = pattern LEVEL "0" -> { (p, Explicit) } ] ]
   ;
   typeclass_constraint:
     [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 22b5e70311..d49a49d242 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -327,6 +327,8 @@ module Constr =
     let binder = Entry.create "binder"
     let binders = Entry.create "binders"
     let open_binders = Entry.create "open_binders"
+    let one_open_binder = Entry.create "one_open_binder"
+    let one_closed_binder = Entry.create "one_closed_binder"
     let binders_fixannot = Entry.create "binders_fixannot"
     let typeclass_constraint = Entry.create "typeclass_constraint"
     let record_declaration = Entry.create "record_declaration"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ce4c91d51f..d0ae594db1 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -203,6 +203,8 @@ module Constr :
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
     val open_binders : local_binder_expr list Entry.t
+    val one_open_binder : kinded_cases_pattern_expr Entry.t
+    val one_closed_binder : kinded_cases_pattern_expr Entry.t
     val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index aab385a707..b64c2b956a 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -36,9 +36,11 @@ let ppcmd_of_cut = function
   | PpFnl -> fnl ()
   | PpBrk(n1,n2) -> brk(n1,n2)
 
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
 type unparsing =
   | UnpMetaVar of entry_relative_level * Extend.side option
-  | UnpBinderMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level * pattern_quote_style
   | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
@@ -50,7 +52,7 @@ type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
   | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
-  | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpBinderMetaVar (p1,s1), UnpBinderMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
   | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2
   | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 56a3fc8e3c..ca22aacacf 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -28,10 +28,12 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** {6 Printing rules for notations} *)
 
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
   | UnpMetaVar of entry_relative_level * Extend.side option
-  | UnpBinderMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level * pattern_quote_style
   | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 54fdea0860..74535a10d3 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -141,7 +141,7 @@ let interp_search_notation ?loc tag okey =
   let rec sub () = function
   | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
-    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x t -> (), None, x, Explicit, t) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
   Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e312c68b7d..8942bc7805 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -98,10 +98,10 @@ let tag_var = tag Tag.variable
         let pp2 = aux l in
         let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in
         return unp pp1 pp2
-      | UnpBinderMetaVar prec as unp :: l ->
-        let c = pop bl in
+      | UnpBinderMetaVar (prec,style) as unp :: l ->
+        let c,bk = pop bl in
         let pp2 = aux l in
-        let pp1 = pr_patt prec c in
+        let pp1 = pr_patt prec style bk c in
         return unp pp1 pp2
       | UnpListMetaVar (prec, sl, side) as unp :: l ->
         let cl = pop envlist in
@@ -273,28 +273,29 @@ let tag_var = tag Tag.variable
   let las = lapp
   let lpator = 0
   let lpatrec = 0
+  let lpatcast = LevelLe 100
   let lpattop = LevelLe 200
 
-  let rec pr_patt sep inh p =
+  let rec pr_patt sep pr inh p =
     let (strm,prec) = match CAst.(p.v) with
       | CPatRecord l ->
-        pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec
+        pr_record_body "{|" "|}" (pr_patt spc pr lpattop) l, lpatrec
 
       | CPatAlias (p, na) ->
-        pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
+        pr_patt mt pr (LevelLe las) p ++ str " as " ++ pr_lname na, las
 
       | CPatCstr (c, None, []) ->
         pr_reference c, latom
 
       | CPatCstr (c, None, args) ->
-        pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
+        pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp
 
       | CPatCstr (c, Some args, []) ->
-        str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
+        str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp
 
       | CPatCstr (c, Some expl_args, extra_args) ->
-        surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args)
-        ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp
+        surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) expl_args)
+        ++ prlist (pr_patt spc pr (LevelLt lapp)) extra_args, lapp
 
       | CPatAtom (None) ->
         str "_", latom
@@ -303,25 +304,25 @@ let tag_var = tag Tag.variable
         pr_reference r, latom
 
       | CPatOr pl ->
-        let pp p = hov 0 (pr_patt mt lpattop p) in
+        let pp p = hov 0 (pr_patt mt pr lpattop p) in
         surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
 
       | CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
-        pr_patt (fun()->str"(") lpattop p ++ str")", latom
+        pr_patt (fun()->str"(") pr lpattop p ++ str")", latom
 
       | CPatNotation (which,s,(l,ll),args) ->
-        let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
+        let strm_not, l_not = pr_notation (pr_patt mt pr) (fun _ _ _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
         (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not)
-        ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
+        ++ prlist (pr_patt spc pr (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
 
       | CPatPrim p ->
         pr_prim_token p, latom
 
       | CPatDelimiters (k,p) ->
-        pr_delimiters k (pr_patt mt lsimplepatt p), 1
+        pr_delimiters k (pr_patt mt pr lsimplepatt p), 1
 
-      | CPatCast _ ->
-        assert false
+      | CPatCast (p,t) ->
+        (pr_patt mt pr lpatcast p ++ spc () ++ str ":" ++ ws 1 ++ pr t), 1
     in
     let loc = p.CAst.loc in
     pr_with_comments ?loc
@@ -329,12 +330,21 @@ let tag_var = tag Tag.variable
 
   let pr_patt = pr_patt mt
 
+  let pr_patt_binder pr prec style bk c =
+    match bk with
+    | MaxImplicit -> str "{" ++ pr_patt pr lpattop c ++ str "}"
+    | NonMaxImplicit -> str "[" ++ pr_patt pr lpattop c ++ str "]"
+    | Explicit ->
+      match style, c with
+      | NotQuotedPattern, _ | _, {v=CPatAtom _} -> pr_patt pr prec c
+      | QuotedPattern, _ -> str "'" ++ pr_patt pr prec c
+
   let pr_eqn pr {loc;v=(pl,rhs)} =
     spc() ++ hov 4
       (pr_with_comments ?loc
          (str "| " ++
             hov 0 (prlist_with_sep pr_spcbar
-                     (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt ltop) p)) pl
+                     (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt (pr ltop) ltop) p)) pl
                    ++ str " =>") ++
             pr_sep_com spc (pr ltop) rhs))
 
@@ -391,13 +401,8 @@ let tag_var = tag Tag.variable
       surround (pr_lname na ++
                 pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
                 str" :=" ++ spc() ++ pr_c c)
-    | CLocalPattern {CAst.loc; v = p,tyo} ->
-      let p = pr_patt lsimplepatt p in
-      match tyo with
-        | None ->
-          str "'" ++ p
-        | Some ty ->
-          str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
+    | CLocalPattern p ->
+      str "'" ++ pr_patt pr_c lsimplepatt p
 
   let pr_undelimited_binders sep pr_c =
     prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -459,16 +464,16 @@ let tag_var = tag Tag.variable
         (pr_decl "with" true) dl ++
         fnl() ++ keyword "for" ++ spc () ++ pr_id id
 
-  let pr_asin pr na indnalopt =
+  let pr_as_in pr na indnalopt =
     (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
       | Some na -> spc () ++ keyword "as" ++ spc () ++  pr_lname na
       | None -> mt ()) ++
       (match indnalopt with
         | None -> mt ()
-        | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
+        | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt pr lsimplepatt t)
 
   let pr_case_item pr (tm,as_clause, in_clause) =
-    hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause)
+    hov 0 (pr (LevelLe lcast) tm ++ pr_as_in (pr ltop) as_clause in_clause)
 
   let pr_case_type pr po =
     match po with
@@ -601,8 +606,8 @@ let tag_var = tag Tag.variable
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
-              hov 0 (pr_patt ltop p ++
-                       pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
+              hov 0 (pr_patt (pr mt ltop) ltop p ++
+                       pr_as_in (pr mt ltop) as_clause in_clause ++
                        str " :=" ++ pr spc ltop c ++
                        pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
                        spc () ++ keyword "in" ++ pr spc ltop b)),
@@ -673,7 +678,7 @@ let tag_var = tag Tag.variable
       | CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
         return (pr (fun()->str"(") ltop t ++ str")", latom)
       | CNotation (which,s,env) ->
-        pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
+        pr_notation (pr mt) (pr_patt_binder (pr mt ltop)) (pr_binders_gen (pr mt ltop)) which s env
       | CGeneralization (bk,ak,c) ->
         return (pr_generalization bk ak (pr mt ltop c), latom)
       | CPrim p ->
@@ -737,7 +742,7 @@ let tag_var = tag Tag.variable
   let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
   let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
 
-  let pr_cases_pattern_expr = pr_patt ltop
+  let pr_cases_pattern_expr = pr_patt (pr ltop) ltop
 
   let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop)
 
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b2ebc61b4e..9bf765717f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -433,7 +433,8 @@ let match_goals ot nt =
         constr_expr ogname c c2;
         constr_expr_opt ogname t t2
       | CLocalPattern p, CLocalPattern p2 ->
-        let (p,ty), (p2,ty2) = p.v,p2.v in
+        let ty = match p.v with CPatCast (_,ty) -> Some ty | _ -> None in
+        let ty2 = match p2.v with CPatCast (_,ty) -> Some ty | _ -> None in
         constr_expr_opt ogname ty ty2
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
     in
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 86c4b3cccc..df64ae2af3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -197,3 +197,15 @@ Found an inductive type while a pattern was expected.
      : nat * nat
 %%%
      : Type
+## (x, _) (x = 0)
+     : Prop
+The command has indeed failed with message:
+Unexpected type constraint in notation already providing a type constraint.
+## '(x, y) (x + y = 0)
+     : Prop
+## x (x = 0)
+     : Prop
+## '(x, y) (x = 0)
+     : Prop
+fun f : ## a (a = 0) => f 1 eq_refl
+     : ## a (a = 0) -> 1 = 0
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6af192ea82..ebc1426fc8 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -487,3 +487,21 @@ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
 Check %%%.
 
 End MorePrecise3.
+
+Module TypedPattern.
+
+Notation "## x P" := (forall x:nat*nat, P) (x pattern, at level 0).
+Check ## (x,y) (x=0).
+Fail Check ## ((x,y):bool*bool) (x=y).
+
+End TypedPattern.
+
+Module SingleBinder.
+
+Notation "## x P" := (forall x, x = x -> P) (x binder, at level 0).
+Check ## '(x,y) (x+y=0).
+Check ## (x:nat) (x=0).
+Check ## '((x,y):nat*nat) (x=0).
+Check fun (f : ## {a} (a=0)) => f (a:=1) eq_refl.
+
+End SingleBinder.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index efe4e17d0b..ad6ac8d3f3 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,6 +249,7 @@ type (_, _) entry =
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
+| TTBinder : bool -> ('self, kinded_cases_pattern_expr) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -364,6 +365,8 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
 | TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
 | TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder)
+| TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder)
 | TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
 | TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
 | TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
@@ -372,6 +375,7 @@ let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
+| ETProdOneBinder o -> TTAny (TTBinder o)
 | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
 | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -385,7 +389,7 @@ let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binders : cases_pattern_expr list;
+  binders : kinded_cases_pattern_expr list;
   binderlists : local_binder_expr list list;
 }
 
@@ -396,14 +400,15 @@ match e with
 | TTConstr _ -> push_constr subst v
 | TTName ->
   begin match forpat with
-  | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
+  | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders }
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
 | TTPattern _ ->
   begin match forpat with
-  | ForConstr -> { subst with binders = v :: subst.binders }
+  | ForConstr -> { subst with binders = (v, Glob_term.Explicit) :: subst.binders }
   | ForPattern -> push_constr subst v
   end
+| TTBinder o -> { subst with binders = v :: subst.binders }
 | TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
 | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index dc2b2e889e..8759798331 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -342,12 +342,10 @@ let unparsing_metavar i from typs =
   match x with
   | ETConstr _ | ETGlobal | ETBigint ->
      UnpMetaVar (prec,side)
-  | ETPattern _ ->
-     UnpBinderMetaVar prec
-  | ETIdent ->
-     UnpBinderMetaVar prec
-  | ETBinder isopen ->
-     assert false
+  | ETPattern _ | ETIdent ->
+     UnpBinderMetaVar (prec,NotQuotedPattern)
+  | ETBinder _ ->
+     UnpBinderMetaVar (prec,QuotedPattern)
 
 (* Heuristics for building default printing rules *)
 
@@ -636,7 +634,7 @@ let prod_entry_type = function
   | ETIdent -> ETProdName
   | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
-  | ETBinder _ -> assert false (* See check_binder_type *)
+  | ETBinder o -> ETProdOneBinder o
   | ETConstr (s,_,p) -> ETProdConstr (s,p)
   | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
 
@@ -970,15 +968,6 @@ let check_useless_entry_types recvars mainvars etyps =
                   (Id.print x ++ str " is unbound in the notation.")
   | _ -> ()
 
-let check_binder_type recvars etyps =
-  let l1,l2 = List.split recvars in
-  let l = l1@l2 in
-  List.iter (function
-    | (x,ETBinder b) when not (List.mem x l) ->
-       CErrors.user_err (str (if b then "binder" else "closed binder") ++
-                 strbrk " is only for use in recursive notations for binders.")
-    | _ -> ()) etyps
-
 let interp_non_syntax_modifiers mods =
   let set modif (only_parsing,only_printing,entry) = match modif with
     | SetOnlyParsing -> Some (true,only_printing,entry)
@@ -1058,7 +1047,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function
   | ETBigint | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
-     else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+     else NtnTypeBinder NtnParsedAsBinder
 
 let subentry_of_constr_prod_entry from_level = function
   (* Specific 8.2 approximation *)
@@ -1297,7 +1286,6 @@ let compute_syntax_data ~local deprecation df modifiers =
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
-  let _ = check_binder_type recvars mods.etyps in
 
   (* Notations for interp and grammar  *)
   let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in