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

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

8 files changed, 215 insertions, 127 deletions

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