Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

13 files changed, 1086 insertions, 748 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index da04d8786b..8aca6e3333 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -67,7 +67,7 @@ let rec cases_pattern_expr_eq p1 p2 =
   if CAst.(p1.v == p2.v) then true
   else match CAst.(p1.v, p2.v) with
   | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
-      Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
+      Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       eq_reference c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -112,10 +112,10 @@ let rec constr_expr_eq e1 e2 =
       eq_located Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
     | CProdN(bl1,a1), CProdN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
       Name.equal na1 na2 &&
@@ -193,10 +193,6 @@ and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
   List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
-and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
-  (** Don't care about the [binder_kind] *)
-  List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
-
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
   (eq_located Id.equal id1 id2) &&
   Option.equal (eq_located Id.equal) j1 j2 &&
@@ -226,9 +222,10 @@ and local_binder_eq l1 l2 = match l1, l2 with
     List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
-and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
+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 (List.equal local_binder_eq) bl1 bl2
 
 and instance_eq (x1,c1) (x2,c2) =
@@ -272,7 +269,7 @@ let is_constructor id =
 let rec cases_pattern_fold_names f a 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,id) -> f id a
+  | CPatAlias (pat,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
   | CPatOr (patl) ->
     List.fold_left (cases_pattern_fold_names f) a patl
   | CPatCstr (_,patl1,patl2) ->
@@ -307,14 +304,6 @@ let ids_of_cases_tomatch tms =
          (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
-let rec fold_constr_expr_binders g f n acc b = function
-  | (nal,bk,t)::l ->
-    let nal = snd (List.split nal) in
-    let n' = List.fold_right (Name.fold_right g) nal n in
-    f n (fold_constr_expr_binders g f n' acc b l) t
-  | [] ->
-    f n acc b
-
 let rec fold_local_binders g f n acc b = function
   | CLocalAssum (nal,bk,t)::l ->
     let nal = snd (List.split nal) in
@@ -331,12 +320,12 @@ let rec fold_local_binders g f n acc b = function
 let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
     | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
-    | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
+    | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
     | CCast (a,CastCoerce) -> f n acc a
-    | CNotation (_,(l,ll,bll)) ->
+    | CNotation (_,(l,ll,bl,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
@@ -382,12 +371,6 @@ let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 (* Used in correctness and interface *)
 let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
 
-let map_binders f g e bl =
-  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in
-  let (e,rbl) = List.fold_left h (e,[]) bl in
-  (e, List.rev rbl)
-
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let h (e,bl) = function
@@ -406,15 +389,15 @@ 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_binders f g e bl in CProdN (bl,f e b)
+      let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
-      let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
+      let (e,bl) = 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 (snd na) e) b)
     | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
-    | CNotation (n,(l,ll,bll)) ->
+    | CNotation (n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
-      CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll,
+      CNotation (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))
     | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
     | CDelimiters (s,a) -> CDelimiters (s,f e a)
@@ -473,9 +456,10 @@ let locs_of_notation ?loc locs ntn =
     | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l
   in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)
 
-let ntn_loc ?loc (args,argslist,binderslist) =
+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 local_binders_loc binderslist)
 
 let patntn_loc ?loc (args,argslist) =
@@ -529,9 +513,9 @@ let split_at_annot bl na =
 let mkIdentC id   = CAst.make @@ CRef (Ident (Loc.tag id),None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k) = CAst.make @@ CCast (a,k)
-let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
@@ -539,56 +523,11 @@ let mkAppC (f,l) =
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
   | _           -> CAst.make @@ CApp ((None, f), l)
 
-let add_name_in_env env n =
-  match snd n with
-  | Anonymous -> env
-  | Name id -> id :: env
-
-let fresh_var env c =
-  Namegen.next_ident_away (Id.of_string "pat")
-    (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env)
-
-let expand_binders ?loc mkC bl c =
-  let rec loop ?loc bl c =
-    match bl with
-    | [] -> ([], c)
-    | b :: bl ->
-      match b with
-      | CLocalDef ((loc1,_) as n, oty, b) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = add_name_in_env env n in
-        (env, CAst.make ?loc @@ CLetIn (n,oty,b,c))
-      | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = List.fold_left add_name_in_env env nl in
-        (env, mkC ?loc (nl,bk,t) c)
-      | CLocalAssum ([],_,_) -> loop ?loc bl c
-      | CLocalPattern (loc1, (p, ty)) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let ni = fresh_var env c in
-        let id = (loc1, Name ni) in
-        let ty = match ty with
-          | Some ty -> ty
-          | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
-        in
-        let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in
-        let c = CAst.make ?loc @@
-          CCases
-            (LetPatternStyle, None, [(e,None,None)],
-             [(Loc.tag ?loc:loc1 ([[p]], c))])
-        in
-        (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
-  in
-  let (_, c) = loop ?loc bl c in
-  c
-
 let mkCProdN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CProdN (bll,c)
 
 let mkCLambdaN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CLambdaN (bll,c)
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
@@ -608,6 +547,49 @@ let coerce_to_name = function
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
+let mkCPatOr ?loc = function
+  | [pat] -> pat
+  | disjpat -> CAst.make ?loc @@ (CPatOr disjpat)
+
+let mkAppPattern ?loc p lp =
+  let open CAst in
+  make ?loc @@ (match p.v with
+  | CPatAtom (Some r) -> CPatCstr (r, None, lp)
+  | CPatCstr (r, None, l2) ->
+     CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
+                      (Pp.str "Nested applications not supported.")
+  | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
+  | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+  | _ -> CErrors.user_err
+           ?loc:p.loc ~hdr:"compound_pattern"
+           (Pp.str "Such pattern cannot have arguments."))
+
+let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
+  | CRef (r,None) ->
+     CPatAtom (Some r)
+  | CHole (None,Misctypes.IntroAnonymous,None) ->
+     CPatAtom None
+  | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+      CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id))
+  | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
+     (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
+  | CAppExpl ((None,r,i),args) ->
+     CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
+  | CNotation (ntn,(c,cl,[],[])) ->
+     CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+                        List.map (List.map coerce_to_cases_pattern_expr) cl),[])
+  | CPrim p ->
+     CPatPrim p
+  | CRecord l ->
+     CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
+  | CDelimiters (s,p) ->
+     CPatDelimiters (s,coerce_to_cases_pattern_expr p)
+  | CCast (p,CastConv t) ->
+     CPatCast (coerce_to_cases_pattern_expr p,t)
+  | _ ->
+     CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
+                      (str "This expression should be coercible to a pattern.")) c
+
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr = false;
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 6e5c0f8515..0b00b0e4dc 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -54,6 +54,11 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e
 val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
+val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
+
+val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
+(** Apply a list of pattern arguments to a pattern *)
+
 (** @deprecated variant of mkCLambdaN *)
 val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
 [@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
@@ -73,6 +78,8 @@ val coerce_to_id : constr_expr -> Id.t located
 val coerce_to_name : constr_expr -> Name.t located
 (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
 
+val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
+
 (** {6 Binder manipulation} *)
 
 val default_binder_kind : binder_kind
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4f7d537d3f..9e18966b63 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function
 
 let insert_pat_alias ?loc p = function
   | Anonymous -> p
-  | Name id -> CAst.make ?loc @@ CPatAlias (p,id)
+  | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na))
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -323,34 +323,35 @@ let is_zero s =
     Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
   in aux 0
 
-let make_notation_gen loc ntn mknot mkprim destprim l =
+let make_notation_gen loc ntn mknot mkprim destprim l bl =
   match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
-        mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
+        assert (bl=[]);
+        mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[])
     | _ ->
 	match decompose_notation_key ntn, l with
 	| [Terminal "-"; Terminal x], [] when is_number x ->
 	   mkprim (loc, Numeral (x,false))
 	| [Terminal x], [] when is_number x ->
 	   mkprim (loc, Numeral (x,true))
-	| _ -> mknot (loc,ntn,l)
+        | _ -> mknot (loc,ntn,l,bl)
 
-let make_notation loc ntn (terms,termlists,binders as subst) =
-  if not (List.is_empty termlists) || not (List.is_empty binders) then
+let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
+  if not (List.is_empty termlists) || not (List.is_empty binderlists) then
     CAst.make ?loc @@ CNotation (ntn,subst)
   else
     make_notation_gen loc ntn
-      (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[])))
+      (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[])))
       (fun (loc,p) -> CAst.make ?loc @@ CPrim p)
-      destPrim terms
+      destPrim terms binders
 
 let make_pat_notation ?loc ntn (terms,termlists as subst) args =
   if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+    (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
     (fun (loc,p)     -> CAst.make ?loc @@ CPatPrim p)
-    destPatPrim terms
+    destPatPrim terms []
 
 let mkPat ?loc qid l = CAst.make ?loc @@
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
@@ -533,6 +534,10 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
 let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
@@ -817,13 +822,11 @@ let rec extern inctx scopes vars r =
 
   | GProd (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
-      let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
-      CProdN ([(Loc.tag na)::idl,Default bk,t],c)
+      factorize_prod scopes (add_vname vars na) na bk t c
 
   | GLambda (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
-      let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in
-      CLambdaN ([(Loc.tag na)::idl,Default bk,t],c)
+      factorize_lambda inctx scopes (add_vname vars na) na bk t c
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -919,24 +922,60 @@ and extern_typ (_,scopes) =
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
 and factorize_prod scopes vars na bk aty c =
-  let c = extern_typ scopes vars c in
-  match na, c with
-  | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) }
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
-      nal,c
-  | _ ->
-      [],c
+  let store, get = set_temporary_memory () in
+  match na, DAst.get c with
+  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+         when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
+    (match get () with
+     | [(_,(ids,disj_of_patl,b))] ->
+      let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
+      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 (c.loc,(p,None)) in
+      (match b.v with
+      | CProdN (bl,b) -> CProdN (binder::bl,b)
+      | _ -> CProdN ([binder],b))
+     | _ -> assert false)
+  | _, _ ->
+      let c = extern_typ scopes vars c in
+      match na, c.v with
+      | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
+           when binding_kind_eq bk bk' && constr_expr_eq aty ty
+                && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
+         CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+      | _, CProdN (bl,b) ->
+         CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+      | _, _ ->
+         CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
 
 and factorize_lambda inctx scopes vars na bk aty c =
-  let c = sub_extern inctx scopes vars c in
-  match c with
-  | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) }
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
-      nal,c
-  | _ ->
-      [],c
+  let store, get = set_temporary_memory () in
+  match na, DAst.get c with
+  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+         when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
+    (match get () with
+     | [(_,(ids,disj_of_patl,b))] ->
+      let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
+      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 (c.loc,(p,None)) in
+      (match b.v with
+      | CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
+      | _ -> CLambdaN ([binder],b))
+     | _ -> assert false)
+  | _, _ ->
+      let c = sub_extern inctx scopes vars c in
+      match c.v with
+      | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
+           when binding_kind_eq bk bk' && constr_expr_eq aty ty
+                && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+         CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+      | CLambdaN (bl,b) ->
+         CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+      | _ ->
+         CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
@@ -965,7 +1004,7 @@ and extern_local_binder scopes vars = function
     | GLocalPattern ((p,_),_,bk,ty) ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
-      let p = extern_cases_pattern vars p 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(Loc.tag @@ (p,ty)) :: l)
 
@@ -1014,7 +1053,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
           | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
-	let terms,termlists,binders =
+        let terms,termlists,binders,binderlists =
           match_notation_constr !print_universes t pat in
 	(* Try availability of interpretation ... *)
         let e =
@@ -1035,11 +1074,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
 		    List.map (fun (c,(scopt,scl)) ->
 		      List.map (extern true (scopt,scl@scopes') vars) c)
                       termlists in
-		  let bll =
-		    List.map (fun (bl,(scopt,scl)) ->
-		      pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
+                  let bl =
+                    List.map (fun (bl,(scopt,scl)) ->
+                      mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl))
                       binders in
-	          insert_delimiters (make_notation loc ntn (l,ll,bll)) key)
+                  let bll =
+                    List.map (fun (bl,(scopt,scl)) ->
+		      pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
+                      binderlists in
+                  insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)
           | SynDefRule kn ->
 	      let l =
 		List.map (fun (c,(scopt,scl)) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4afe301dd7..694bec8972 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -213,20 +213,20 @@ let expand_notation_string ntn n =
 
 (* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
 (* Remark: expansion of squash at definition is done in metasyntax.ml *)
-let contract_notation ntn (l,ll,bll) =
+let contract_curly_brackets ntn (l,ll,bl,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l ->
+    | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  !ntn',(l,ll,bll)
+  !ntn',(l,ll,bl,bll)
 
-let contract_pat_notation ntn (l,ll) =
+let contract_curly_brackets_pat ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
@@ -271,29 +271,24 @@ let error_expect_binder_notation_type ?loc id =
    (Id.print id ++
     str " is expected to occur in binding position in the right-hand side.")
 
-let set_var_scope ?loc id istermvar env ntnvars =
+let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
   try
-    let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
-    if istermvar then isonlybinding := false;
+    let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
+    if not istermvar then used_as_binder := true;
     let () = if istermvar then
       (* scopes have no effect on the interpretation of identifiers *)
       begin match !idscopes with
-      | None -> idscopes := Some (env.tmp_scope, env.scopes)
-      | Some (tmp, scope) ->
-        let s1 = make_current_scope tmp scope in
-        let s2 = make_current_scope env.tmp_scope env.scopes in
-        if not (List.equal String.equal s1 s2) then error_inconsistent_scope ?loc id s1 s2
+      | 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
       end
     in
     match typ with
-    | NtnInternTypeBinder ->
+    | Notation_term.NtnInternTypeOnlyBinder ->
 	if istermvar then error_expect_binder_notation_type ?loc id
-    | NtnInternTypeConstr ->
-	(* We need sometimes to parse idents at a constr level for
-	   factorization and we cannot enforce this constraint:
-	   if not istermvar then error_expect_constr_notation_type loc id *)
-	()
-    | NtnInternTypeIdent -> ()
+    | Notation_term.NtnInternTypeAny -> ()
   with Not_found ->
     (* Not in a notation *)
     ()
@@ -302,15 +297,11 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
-let rec it_mkGProd ?loc env body =
-  match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
-    | [] -> body
+let set_env_scopes env (scopt,subscopes) =
+  {env with tmp_scope = scopt; scopes = subscopes @ env.scopes}
 
-let rec it_mkGLambda ?loc env body =
-  match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
-    | [] -> body
+let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body)
+let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
@@ -378,12 +369,12 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
       check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
-      set_var_scope ?loc id false env ntnvars;
+      set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding ?loc id;
       {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
-let intern_generalized_binder ?(global_level=false) intern_type lvar
+let intern_generalized_binder ?(global_level=false) intern_type ntnvars
     env (loc, na) b b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
@@ -394,7 +385,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env (l, x) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
+    (fun env (l, x) -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (l, Name x))
     env fvs in
   let bl = List.map
     (fun (loc, id) ->
@@ -413,9 +404,9 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl
+  in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl
 
-let intern_assumption intern lvar env nal bk ty =
+let intern_assumption intern ntnvars env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
   match bk with
   | Default k ->
@@ -424,11 +415,11 @@ let intern_assumption intern lvar env nal bk ty =
       let impls = impls_type_list ty in
       List.fold_left
 	(fun (env, bl) (loc, na as locna) ->
-          (push_name_env lvar impls env locna,
+          (push_name_env ntnvars impls env locna,
            (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
-     let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
+     let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
      env, b
 
 let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
@@ -443,39 +434,48 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
-let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
+let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) =
+  let term = intern env def in
+  let ty = Option.map (intern env) ty in
+  (push_name_env ntnvars (impls_term_list term) env locna,
+   (na,Explicit,term,ty))
+
+let intern_cases_pattern_as_binder ?loc ntnvars env p =
+  let il,disjpat =
+    let (il, subst_disjpat) = !intern_cases_pattern_fwd ntnvars (None,env.scopes) p in
+    let substl,disjpat = List.split subst_disjpat in
+    if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then
+      user_err ?loc (str "Unsupported nested \"as\" clause.");
+    il,disjpat
+  in
+  let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in
+  let na = alias_of_pat (List.hd disjpat) 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 = (loc, Name id) in
+  env,((disjpat,il),id),na
+
+let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
-      let env, bl' = intern_assumption intern lvar env nal bk ty in
+      let env, bl' = intern_assumption intern ntnvars env nal bk ty in
       let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def,ty) ->
-     let term = intern env def in
-     let ty = Option.map (intern env) ty in
-      (push_name_env lvar (impls_term_list term) env locna,
-       (DAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+     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,(p,ty)) ->
       let tyc =
         match ty with
         | Some ty -> ty
         | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
-      let il,cp =
-        match !intern_cases_pattern_fwd (None,env.scopes) p with
-        | (il, [(subst,cp)]) ->
-           if not (Id.Map.equal Id.equal subst Id.Map.empty) then
-             user_err ?loc (str "Unsupported nested \"as\" clause.");
-           il,cp
-        | _ -> assert false
-      in
-      let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
-      let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in
-      let na = (loc, Name id) in
+      let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
       let bk = Default Explicit in
-      let _, bl' = intern_assumption intern lvar env [na] bk tyc in
+      let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
       let _,(_,bk,t) = List.hd bl' in
-      (env, (DAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
+      (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map snd il),id,bk,t)) :: bl)
 
-let intern_generalization intern env lvar loc bk ak c =
+let intern_generalization intern env ntnvars loc bk ak c =
   let c = intern {env with unb = true} c in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in
   let env', c' =
@@ -504,10 +504,26 @@ let intern_generalization intern env lvar loc bk ak c =
 	    GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
       List.fold_right (fun (loc, id as lid) (env, acc) ->
-	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
+        let env' = push_name_env ntnvars (Variable,[],[],[]) env (loc, Name id) in
 	  (env', abs lid acc)) fvs (env,c)
   in c'
 
+let rec expand_binders ?loc mk bl c =
+  match bl with
+  | [] -> c
+  | b :: bl ->
+     match DAst.get b with
+     | GLocalDef (n, bk, b, oty) ->
+        expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c))
+     | GLocalAssum (n, bk, t) ->
+        expand_binders ?loc mk bl (mk ?loc (n,bk,t) c)
+     | GLocalPattern ((disjpat,ids), id, bk, ty) ->
+        let tm = DAst.make ?loc (GVar id) in
+        (* Distribute the disjunctive patterns over the shared right-hand side *)
+        let eqnl = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in
+        let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
+        expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
+
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
@@ -515,7 +531,7 @@ let option_mem_assoc id = function
   | Some (id',c) -> Id.equal id id'
   | None -> false
 
-let find_fresh_name renaming (terms,termlists,binders) avoid id =
+let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
   let fold1 _ (c, _) accu = Id.Set.union (free_vars_of_constr_expr c) accu in
   let fold2 _ (l, _) accu =
     let fold accu c = Id.Set.union (free_vars_of_constr_expr c) accu in
@@ -528,14 +544,53 @@ let find_fresh_name renaming (terms,termlists,binders) avoid id =
   (* TODO binders *)
   next_ident_away_from id (fun id -> Id.Set.mem id fvs3)
 
-let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env),Anonymous
+let is_var store pat =
+  match DAst.get pat with
+  | PatVar na -> store na; true
+  | _ -> false
+
+let out_var pat =
+  match pat.CAst.v with
+  | CPatAtom (Some (Ident (_,id))) -> Name id
+  | CPatAtom None -> Anonymous
+  | _ -> assert false
+
+let term_of_name = function
+  | Name id -> DAst.make (GVar id)
+  | Anonymous ->
+       let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+
+let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
+ | Anonymous -> (renaming,env), None, Anonymous
  | Name id ->
+  let store,get = set_temporary_memory () 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 ntnvars env pat in
+    let pat, na = match disjpat with
+    | [pat] when is_var store pat -> let na = get () in None, na
+    | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+    (renaming,env), pat, na
+  with Not_found ->
   try
-    (* Binders bound in the notation are considered first-order objects *)
-    let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in
-    let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in
-    (renaming,env), na
+    (* Trying to associate a pattern *)
+    let pat,(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_var pat in
+      let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+      (renaming,env), None, na
+    else
+      (* Interpret as a pattern *)
+      let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+      let pat, na =
+        match disjpat with
+        | [pat] when is_var store pat -> let na = get () in None, na
+        | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+      (renaming,env), pat, na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -543,49 +598,27 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
     let renaming' =
       if Id.equal id id' then renaming else Id.Map.add id id' renaming
     in
-    (renaming',env), Name id'
-
-type letin_param_r =
-  | LPLetIn of Name.t * glob_constr * glob_constr option
-  | LPCases of (cases_pattern * Id.t list) * Id.t
-(* Unused thus fatal warning *)
-(* and letin_param = letin_param_r Loc.located *)
-
-let make_letins =
-  List.fold_right
-    (fun a c ->
-     match a with
-     | loc, LPLetIn (na,b,t) ->
-       DAst.make ?loc @@ GLetIn(na,b,t,c)
-     | loc, LPCases ((cp,il),id) ->
-         let tt = (DAst.make ?loc @@ GVar id, (Name id,None)) in
-         DAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
-
-let rec subordinate_letins letins l = match l with
-  | bnd :: l ->
-    let loc = bnd.CAst.loc in
-    begin match DAst.get bnd with
-  (* binders come in reverse order; the non-let are returned in reverse order together *)
-  (* with the subordinated let-in in writing order *)
-    | GLocalDef (na,_,b,t) ->
-      subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
-    | GLocalAssum (na,bk,t) ->
-      let letins',rest = subordinate_letins [] l in
-      letins',((loc,(na,bk,t)),letins)::rest
-    | GLocalPattern (u,id,bk,t) ->
-      subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
-                          ([DAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
-    end
-  | [] ->
-      letins,[]
+    (renaming',env), None, Name id'
+
+type binder_action =
+| AddLetIn of Name.t Loc.located * constr_expr * constr_expr option
+| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
+| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
+| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
 
 let dmap_with_loc f n =
   CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n
 
+let error_cannot_coerce_wildcard_term ?loc () =
+  user_err ?loc Pp.(str "Cannot turn \"_\" into a term.")
+
+let error_cannot_coerce_disjunctive_pattern_term ?loc () =
+  user_err ?loc Pp.(str "Cannot turn a disjunctive pattern into a term.")
+
 let terms_of_binders bl =
   let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
     | PatVar (Name id)   -> CRef (Ident (loc,id), None)
-    | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
+    | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
        let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
@@ -599,40 +632,62 @@ let terms_of_binders bl =
       | GLocalDef (Name id,_,_,_) -> extract_variables l
       | GLocalDef (Anonymous,_,_,_)
       | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
-      | GLocalPattern ((u,_),_,_,_) -> term_of_pat u :: extract_variables l
+      | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l
+      | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc ()
       end
     | [] -> [] in
   extract_variables bl
 
-let instantiate_notation_constr loc intern ntnvars subst infos c =
-  let (terms,termlists,binders) = subst in
+let flatten_generalized_binders_if_any y l =
+  match List.rev l with
+  | [] -> assert false
+  | a::l -> a, List.map (fun a -> AddBinderIter (y,a)) l (* if l not empty, this means we had a generalized binder *)
+
+let flatten_binders bl =
+  let dispatch = function
+    | CLocalAssum (nal,bk,t) -> List.map (fun na -> CLocalAssum ([na],bk,t)) nal
+    | a -> [a] in
+  List.flatten (List.map dispatch bl)
+
+let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
+  let (terms,termlists,binders,binderlists) = subst in
   (* when called while defining a notation, avoid capturing the private binders
      of the expression by variables bound by the notation (see #3892) *)
   let avoid = Id.Map.domain ntnvars in
-  let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c =
+  let rec aux (terms,binderopt,iteropt as subst') (renaming,env) c =
     let subinfos = renaming,{env with tmp_scope = None} in
     match c with
-    | NVar id when Id.equal id ldots_var -> Option.get terminopt
+    | NVar id when Id.equal id ldots_var ->
+        let rec aux_letin env = function
+        | [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator
+        | AddPreBinderIter (y,binder)::rest,terminator,iter ->
+           let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in
+           let binder,extra = flatten_generalized_binders_if_any y binders in
+           aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter
+        | AddBinderIter (y,binder)::rest,terminator,iter ->
+           aux (terms,Some (y,binder),Some (rest,terminator,iter)) (renaming,env) iter
+        | AddTermIter nterms::rest,terminator,iter ->
+           aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter
+        | AddLetIn (na,c,t)::rest,terminator,iter ->
+           let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in
+           DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in
+        aux_letin env (Option.get iteropt)
     | NVar id -> subst_var subst' (renaming, env) id
-    | NList (x,y,iter,terminator,lassoc) ->
+    | NList (x,y,iter,terminator,revert) ->
       let l,(scopt,subscopes) =
         (* All elements of the list are in scopes (scopt,subscopes) *)
         try
           let l,scopes = Id.Map.find x termlists in
-          (if lassoc then List.rev l else l),scopes
+          (if revert then List.rev l else l),scopes
         with Not_found ->
         try
-	  let (bl,(scopt,subscopes)) = Id.Map.find x binders in
+          let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in
 	  let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
-          terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[])
+          terms_of_binders (if revert then bl' else List.rev bl'),(None,[])
         with Not_found ->
           anomaly (Pp.str "Inconsistent substitution of recursive notation.") in
-      let termin = aux (terms,None,None) subinfos terminator in
-      let fold a t =
-        let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
-        aux (nterms,None,Some t) subinfos iter
-      in
-      List.fold_right fold l termin
+      let l = List.map (fun a -> AddTermIter ((Id.Map.add y (a,(scopt,subscopes)) terms))) l in
+      aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
     | NHole (knd, naming, arg) ->
       let knd = match knd with
       | Evar_kinds.BinderType (Name id as na) ->
@@ -653,47 +708,57 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
           let gc = intern nenv c in
           (gc, Some c)
         in
-        let bindings = Id.Map.map mk_env terms in
+        let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
+          let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
+          if onlyident then
+            let na = out_var c in term_of_name na, None
+          else
+            let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
+            match disjpat with
+            | [pat] -> (glob_constr_of_cases_pattern pat, None)
+            | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
+        in
+        let terms = Id.Map.map mk_env terms in
+        let binders = Id.Map.map mk_env' binders in
+        let bindings = Id.Map.fold Id.Map.add terms binders in
         Some (Genintern.generic_substitute_notation bindings arg)
       in
       DAst.make ?loc @@ GHole (knd, naming, arg)
-    | NBinderList (x,y,iter,terminator) ->
+    | NBinderList (x,y,iter,terminator,revert) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
-	let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
-	let letins,bl = subordinate_letins [] bl in
-        let termin = aux (terms,None,None) (renaming,env) terminator in
-	let res = List.fold_left (fun t binder ->
-	    aux (terms,Some(y,binder),Some t) subinfos iter)
-	  termin bl in
-	make_letins letins res
+        let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in
+        (* We flatten binders so that we can interpret them at substitution time *)
+        let bl = flatten_binders bl in
+        let bl = if revert then List.rev bl else bl in
+        (* We isolate let-ins which do not contribute to the repeated pattern *)
+        let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t)
+                                   | binder -> AddPreBinderIter (y,binder)) bl in
+        (* We stack the binders to iterate or let-ins to insert *)
+        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 ->
-        let a,letins = snd (Option.get binderopt) in
-        let e = make_letins letins (aux subst' infos c') in
-        let (_loc,(na,bk,t)) = a in
-        DAst.make ?loc @@ GProd (na,bk,t,e)
+        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 ->
-        let a,letins = snd (Option.get binderopt) in
-        let (_loc,(na,bk,t)) = a in
-        DAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
+        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,na = traverse_binder subst avoid subinfos na in
+        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,aux subst' subinfos c')
+        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,na = traverse_binder subst avoid subinfos na in
+        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,aux subst' subinfos c')
+        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 subst avoid) (aux subst') subinfos t
-  and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
+        (traverse_binder intern_pat ntnvars subst  avoid) (aux subst') subinfos t
+  and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
     try
@@ -701,6 +766,28 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
+    try
+      let pat,(onlyident,scopes) = Id.Map.find id binders in
+      let env = set_env_scopes env scopes in
+      (* We deactivate impls to avoid the check on hidden parameters *)
+      (* and since we are only interested in the pattern as a term *)
+      let env = reset_hidden_inductive_implicit_test env in
+      if onlyident then
+        term_of_name (out_var pat)
+      else
+        let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+        match disjpat with
+        | [pat] -> glob_constr_of_cases_pattern pat
+        | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+    with Not_found ->
+    try
+      match binderopt with
+      | Some (x,binder) when Id.equal x id ->
+         let terms = terms_of_binders [binder] in
+         assert (List.length terms = 1);
+         intern env (List.hd terms)
+      | _ -> raise Not_found
+    with Not_found ->
     DAst.make ?loc (
     try
       GVar (Id.Map.find id renaming)
@@ -709,27 +796,80 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       GVar id)
   in aux (terms,None,None) infos c
 
-let split_by_type ids =
-  List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
+(* Turning substitution coming from parsing and based on production
+   into a substitution for interpretation and based on binding/constr
+   distinction *)
+
+let cases_pattern_of_name (loc,na) =
+  let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
+  CAst.make ?loc (CPatAtom atom)
+
+let split_by_type ids subst =
+  let bind id scl l s =
+    match l with
+    | [] -> assert false
+    | a::l -> l, Id.Map.add id (a,scl) s in
+  let (terms,termlists,binders,binderlists),subst =
+    List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) ->
     match typ with
-    | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3)
-    | NtnTypeConstrList -> (l1,(x,scl)::l2,l3)
-    | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[])
+    | NtnTypeConstr ->
+       let terms,terms' = bind id scl terms terms' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.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
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder NtnBinderParsedAsConstr Extend.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
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ 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')
+    | NtnTypeConstrList ->
+       let termlists,termlists' = bind id scl termlists termlists' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinderList ->
+       let binderlists,binderlists' = bind id scl binderlists binderlists' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists'))
+                   (subst,(Id.Map.empty,Id.Map.empty,Id.Map.empty,Id.Map.empty)) ids in
+  assert (terms = [] && termlists = [] && binders = [] && binderlists = []);
+  subst
+
+let split_by_type_pat ?loc ids subst =
+  let bind id scl l s =
+    match l with
+    | [] -> assert false
+    | a::l -> l, Id.Map.add id (a,scl) s in
+  let (terms,termlists),subst =
+    List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) ->
+    match typ with
+    | NtnTypeConstr | NtnTypeBinder _ ->
+       let terms,terms' = bind id scl terms terms' in
+       (terms,termlists),(terms',termlists')
+    | NtnTypeConstrList ->
+       let termlists,termlists' = bind id scl termlists termlists' in
+       (terms,termlists),(terms',termlists')
+    | NtnTypeBinderList -> error_invalid_pattern_notation ?loc ())
+                   (subst,(Id.Map.empty,Id.Map.empty)) ids in
+  assert (terms = [] && termlists = []);
+  subst
 
 let make_subst ids l =
   let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in
   List.fold_left2 fold Id.Map.empty ids l
 
-let intern_notation intern env lvar loc ntn fullargs =
-  let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
+let intern_notation intern env ntnvars loc ntn fullargs =
+  (* Adjust to parsing of { } *)
+  let ntn,fullargs = contract_curly_brackets ntn fullargs in
+  (* Recover interpretation { } *)
   let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in
   Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df;
-  let ids,idsl,idsbl = split_by_type ids in
-  let terms = make_subst ids args in
-  let termlists = make_subst idsl argslist in
-  let binders = make_subst idsbl bll in
-  instantiate_notation_constr loc intern lvar
-    (terms, termlists, binders) (Id.Map.empty, env) c
+  (* 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
 
 (**********************************************************************)
 (* Discriminating between bound variables and global references       *)
@@ -746,17 +886,17 @@ let gvar (loc, id) us = match us with
   user_err ?loc  (str "Variable " ++ Id.print id ++
     str " cannot have a universe instance")
 
-let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
+let intern_var env (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] a notation variable *)
   if Id.Map.mem id ntnvars then
     begin
-      if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars;
+      if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars;
       gvar (loc,id) us, [], [], []
     end
   else
   (* Is [id] registered with implicit arguments *)
   try
-    let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
+    let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
     let expl_impls = List.map
       (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
@@ -764,7 +904,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
+  if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars
   then
     gvar (loc,id) us, [], [], []
   else if Id.equal id ldots_var
@@ -849,7 +989,7 @@ let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
   | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
 
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid intern env lvar us args =
+let intern_qualid loc qid intern env ntnvars us args =
   match intern_extended_global_of_qualid (loc,qid) with
   | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
@@ -859,10 +999,10 @@ let intern_qualid loc qid intern env lvar us args =
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
       let terms = make_subst ids (List.map fst args1) in
-      let subst = (terms, Id.Map.empty, Id.Map.empty) in
+      let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
       let projapp = match c with NRef _ -> true | _ -> false in
-      let c = instantiate_notation_constr loc intern lvar subst infos c in
+      let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
       let loc = c.CAst.loc in
       let err () =
         user_err ?loc  (str "Notation " ++ pr_qualid qid
@@ -888,8 +1028,8 @@ let intern_qualid loc qid intern env lvar us args =
       c, projapp, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env lvar us args =
-  let c, _, _ as r = intern_qualid loc qid intern env lvar us args in
+let intern_non_secvar_qualid loc qid intern env ntnvars us args =
+  let c, _, _ as r = intern_qualid loc qid intern env ntnvars us args in
   match DAst.get c with
     | GRef (VarRef _, _) -> raise Not_found
     | _ -> r
@@ -929,11 +1069,11 @@ let interp_reference vars r =
 
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
-  | RCPatAlias of 'a raw_cases_pattern_expr * Id.t
+  | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located
   | RCPatCstr  of Globnames.global_reference
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
   (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
-  | RCPatAtom  of Id.t option
+  | RCPatAtom  of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
   | RCPatOr    of 'a raw_cases_pattern_expr list
 and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
 
@@ -993,7 +1133,7 @@ let check_number_of_pattern loc n l =
   if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
-  if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
+  if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then
     user_err ?loc  (str
     "The components of this disjunctive pattern must bind the same variables.")
 
@@ -1059,7 +1199,7 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
       then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom None)::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1232,7 +1372,7 @@ let sort_fields ~complete loc fields completer =
 (** {6 Manage multiple aliases} *)
 
 type alias = {
-  alias_ids : Id.t list;
+  alias_ids : Id.t Loc.located list;
   alias_map : Id.t Id.Map.t;
 }
 
@@ -1243,17 +1383,20 @@ let empty_alias = {
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
      point and a substitution mapping extra aliases to the first one *)
-let merge_aliases aliases id =
-  let alias_ids = aliases.alias_ids @ [id] in
+let merge_aliases aliases (loc,na) =
+  match na with
+  | Anonymous -> aliases
+  | Name id ->
+  let alias_ids = aliases.alias_ids @ [loc,id] in
   let alias_map = match aliases.alias_ids with
   | [] -> aliases.alias_map
-  | id' :: _ -> Id.Map.add id id' aliases.alias_map
+  | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map
   in
   { alias_ids; alias_map; }
 
 let alias_of als = match als.alias_ids with
 | [] -> Anonymous
-| id :: _ -> Name id
+| (_,id) :: _ -> Name id
 
 (** {6 Expanding notations }
 
@@ -1271,6 +1414,8 @@ let is_zero s =
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
+  (* each [pl] is a disjunction of patterns over common identifiers [ids] *)
+  (* We stepwise build a disjunction of patterns [ptaill] over common [ids'] *)
   List.fold_right (fun (ids,pl) (ids',ptaill) ->
     (ids @ ids',
      (* Cartesian prod of the or-pats for the nth arg and the tail args *)
@@ -1281,7 +1426,7 @@ let product_of_cases_patterns aliases idspl =
 
 let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatAtom id as p ->
-    begin match id with Some x when Id.equal x y -> DAst.get t | _ -> p end
+    begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end
   | RCPatCstr (id,l1,l2) ->
     RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
  	       List.map (subst_pat_iterator y t) l2)
@@ -1310,13 +1455,16 @@ let drop_notations_pattern looked_for genv =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
   in
   (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
-  let rec rcp_of_glob x = DAst.(map (function
-    | GVar id -> RCPatAtom (Some id)
+  let rec rcp_of_glob scopes x = DAst.(map (function
+    | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes))
     | GHole (_,_,_) -> RCPatAtom (None)
     | GRef (g,_) -> RCPatCstr (g,[],[])
     | GApp (r, l) ->
       begin match DAst.get r with
-      | GRef (g,_) -> RCPatCstr (g, List.map rcp_of_glob l,[])
+      | GRef (g,_) ->
+        let allscs = find_arguments_scope g in
+        let allscs = simple_adjust_scopes (List.length l) allscs in (* TO CHECK *)
+        RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l,[])
       | _ ->
         CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.")
       end
@@ -1396,27 +1544,25 @@ let drop_notations_pattern looked_for genv =
     | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
-      rcp_of_glob pat
+      rcp_of_glob scopes pat
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
-    | CPatNotation (ntn, fullargs,extrargs) ->
-      let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
+    | CPatNotation (ntn,fullargs,extrargs) ->
+      let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
-      let (ids',idsl',_) = split_by_type ids' in
+      let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
       Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
-      let substlist = make_subst idsl' argsl in
-      let subst = make_subst ids' args in
-      in_not top loc scopes (subst,substlist) extrargs c
+      in_not top loc scopes (terms,termlists) extrargs c
     | CPatDelimiters (key, e) ->
       in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
     | CPatPrim p ->
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in
-      rcp_of_glob pat
-    | CPatAtom Some id ->
+      rcp_of_glob scopes pat
+    | CPatAtom (Some id) ->
       begin
 	match drop_syndef top scopes id [] with
 	  | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
-	  | None         -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
+          | None         -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes))
       end
     | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
     | CPatOr pl     -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
@@ -1446,7 +1592,7 @@ let drop_notations_pattern looked_for genv =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some id) else
+          if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
       end
     | NRef g ->
@@ -1459,7 +1605,7 @@ let drop_notations_pattern looked_for genv =
       let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
       DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
-    | NList (x,y,iter,terminator,lassoc) ->
+    | NList (x,y,iter,terminator,revert) ->
       if not (List.is_empty args) then user_err ?loc 
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
@@ -1470,7 +1616,7 @@ let drop_notations_pattern looked_for genv =
            let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
            let u = in_not false loc scopes (nsubst, substlist) [] iter in
            subst_pat_iterator ldots_var t u)
-           (if lassoc then List.rev l else l) termin
+           (if revert then List.rev l else l) termin
        with Not_found ->
          anomaly (Pp.str "Inconsistent substitution of recursive notation."))
     | NHole _ ->
@@ -1479,9 +1625,9 @@ let drop_notations_pattern looked_for genv =
     | t -> error_invalid_pattern_notation ?loc ()
   in in_pat true
 
-let rec intern_pat genv aliases pat =
+let rec intern_pat genv ntnvars aliases pat =
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
-    let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
+    let idslpl2 = List.map (intern_pat genv ntnvars empty_alias) pl2 in
     let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
@@ -1490,7 +1636,7 @@ let rec intern_pat genv aliases pat =
   match DAst.get pat with
     | RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
-      intern_pat genv aliases' p
+      intern_pat genv ntnvars aliases' p
     | RCPatCstr (head, expl_pl, pl) ->
       if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
@@ -1503,29 +1649,30 @@ let rec intern_pat genv aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | RCPatAtom (Some id) ->
-      let aliases = merge_aliases aliases id in
-      (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)])
+    | RCPatAtom (Some ((loc,id),scopes)) ->
+      let aliases = merge_aliases aliases (loc,Name id) in
+      set_var_scope ?loc id false scopes ntnvars;
+      (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *)
     | RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
       (ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)])
     | RCPatOr pl ->
       assert (not (List.is_empty pl));
-      let pl' = List.map (intern_pat genv aliases) pl in
+      let pl' = List.map (intern_pat genv ntnvars aliases) pl in
       let (idsl,pl') = List.split pl' in
       let ids = List.hd idsl in
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
-let intern_cases_pattern genv scopes aliases pat =
-  intern_pat genv aliases
+let intern_cases_pattern genv ntnvars scopes aliases pat =
+  intern_pat genv ntnvars aliases
     (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
 
 let _ =
   intern_cases_pattern_fwd :=
-    fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
+    fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p
 
-let intern_ind_pattern genv scopes pat =
+let intern_ind_pattern genv ntnvars scopes pat =
   let no_not =
     try
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
@@ -1537,10 +1684,9 @@ let intern_ind_pattern genv scopes pat =
       let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
-      let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
-      let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
+      let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
       (with_letin,
-       match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with
+       match product_of_cases_patterns empty_alias idslpl with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type ?loc)
     | x -> error_bad_inductive_type ?loc
@@ -1697,24 +1843,25 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
-    | CProdN ([],c2) ->
-        intern_type env c2
-    | CProdN ((nal,bk,ty)::bll,c2) ->
-        iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal
+    | CProdN (bl,c2) ->
+        let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
+        expand_binders ?loc mkGProd bl (intern_type env' c2)
     | CLambdaN ([],c2) ->
+        (* Such a term is built sometimes: it should not change scope *)
         intern env c2
-    | CLambdaN ((nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal
+    | CLambdaN (bl,c2) ->
+        let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
+        expand_binders ?loc mkGLambda bl (intern env' c2)
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
 	DAst.make ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _", ([a],[],[])) when is_non_zero a ->
+    | CNotation ("- _", ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
-    | CNotation ("( _ )",([a],[],[])) -> intern env a
+    | CNotation ("( _ )",([a],[],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
     | CGeneralization (b,a,c) ->
@@ -1746,8 +1893,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
-            | CNotation (ntn,([],[],[])) ->
-                let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
+            | CNotation (ntn,([],[],[],[])) ->
+                let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
             | _ -> (intern env f,[],[],[]), args in
@@ -1849,6 +1996,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         | None -> None
         | Some gen ->
           let (ltacvars, ntnvars) = lvar in
+          (* Preventively declare notation variables in ltac as non-bindings *)
+          Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
           let ntnvars = Id.Map.domain ntnvars in
           let extra = ltacvars.ltac_extra in
           let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
@@ -1899,7 +2048,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern env n pl =
-    let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
+    let idsl_pll = List.map (intern_cases_pattern globalenv ntnvars (None,env.scopes) empty_alias) pl in
     let loc = loc_of_multiple_pattern pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns empty_alias idsl_pll
@@ -1917,6 +2066,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
   and intern_eqn n env (loc,(lhs,rhs)) =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
+    let eqn_ids = List.map snd eqn_ids in
     check_linearity lhs eqn_ids;
     let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
@@ -1938,7 +2088,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     (* the "in" part *)
     let match_td,typ = match t with
     | Some t ->
-	let with_letin,(ind,l) = intern_ind_pattern globalenv (None,env.scopes) t in
+        let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
 	let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
 	let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
 	(* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -1979,14 +2129,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
 
-  and iterate_prod ?loc env bk ty body nal =
-    let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGProd ?loc bl (intern_type env body)
-
-  and iterate_lam loc env bk ty body nal =
-    let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGLambda ?loc bl (intern env body)
-
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
     if !parsing_explicit then
@@ -2089,7 +2231,7 @@ let intern_type env c = intern_gen IsType env c
 
 let intern_pattern globalenv patt =
   try
-    intern_cases_pattern globalenv (None,[]) empty_alias patt
+    intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
   with
       InternalizationError (loc,e) ->
 	user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
@@ -2160,7 +2302,8 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
 
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
+  let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
+  let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
@@ -2169,8 +2312,9 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
-  let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
-    (!isonlybinding, out_scope !sc, typ)) vl in
+  let unused = match reversible with NonInjective ids -> ids | _ -> [] in
+  let vars = Id.Map.mapi (fun id (used_as_binder, sc, typ) ->
+    (!used_as_binder && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
   vars, a, reversible
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 632b423b05..f09b17a49f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-  Id.t list * (Id.t Id.Map.t * cases_pattern) list
+  Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list
 
 val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
@@ -184,8 +184,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_
     guaranteed to have the same domain as the input one. *)
 val interp_notation_constr : env -> ?impls:internalization_env ->
   notation_interp_env -> constr_expr ->
-  (bool * subscopes * notation_var_internalization_type) Id.Map.t *
-  notation_constr * reversibility_flag
+  (bool * subscopes) Id.Map.t * notation_constr * reversibility_status
 
 (** Globalization options *)
 val parsing_explicit : bool ref
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 519f2480ba..a838d7106b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -93,8 +93,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   in
   let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (Ident (loc,id),_) -> found loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) ->
-      Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
+        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 94ce2a6c8d..ea7ef21b19 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -82,18 +82,35 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let notation_var_internalization_type_eq v1 v2 = match v1, v2 with
-| NtnInternTypeConstr, NtnInternTypeConstr -> true
-| NtnInternTypeBinder, NtnInternTypeBinder -> true
-| NtnInternTypeIdent, NtnInternTypeIdent -> true
-| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false
-
-let level_eq (l1, t1, u1) (l2, t2, u2) =
-  let tolerability_eq (i1, r1) (i2, r2) =
-    Int.equal i1 i2 && parenRelation_eq r1 r2
-  in
+open Extend
+
+let production_level_eq l1 l2 = true (* (l1 = l2) *)
+
+let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| (NextLevel | NumLevel _), _ -> false *)
+
+let constr_entry_key_eq eq v1 v2 = match v1, v2 with
+| ETName, ETName -> true
+| ETReference, ETReference -> true
+| ETBigint, ETBigint -> true
+| ETBinder b1, ETBinder b2 -> b1 == b2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
+| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+
+let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
+  let prod_eq (l1,pp1) (l2,pp2) =
+    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
+    else production_level_eq l1 l2 in
   Int.equal l1 l2 && List.equal tolerability_eq t1 t2
-  && List.equal notation_var_internalization_type_eq u1 u2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
@@ -292,7 +309,7 @@ let cases_pattern_key c = match DAst.get c with
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_) ->
+  | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
       RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | NApp (_,args) -> Oth, Some (List.length args)
@@ -609,12 +626,18 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
+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
+
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
-| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true
+| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
 | NtnTypeConstrList, NtnTypeConstrList -> true
 | NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
 let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
   pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
@@ -926,8 +949,63 @@ let factorize_entries = function
 	  (ntn,[c],[]) l in
       (ntn,l_of_ntn)::rest
 
+type symbol_token = WhiteSpace of int | String of string
+
+let split_notation_string str =
+  let push_token beg i l =
+    if Int.equal beg i then l else
+      let s = String.sub str beg (i - beg) in
+      String s :: l
+  in
+  let push_whitespace beg i l =
+    if Int.equal beg i then l else WhiteSpace (i-beg) :: l
+  in
+  let rec loop beg i =
+    if i < String.length str then
+      if str.[i] == ' ' then
+        push_token beg i (loop_on_whitespace (i+1) (i+1))
+      else
+        loop beg (i+1)
+    else
+      push_token beg i []
+  and loop_on_whitespace beg i =
+    if i < String.length str then
+      if str.[i] != ' ' then
+        push_whitespace beg i (loop i (i+1))
+      else
+        loop_on_whitespace beg (i+1)
+    else
+      push_whitespace beg i []
+  in
+  loop 0 0
+
+let rec raw_analyze_notation_tokens = function
+  | []    -> []
+  | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_notation_tokens sl
+  | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
+  | String x :: sl when Id.is_valid x ->
+      NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
+  | String s :: sl ->
+      Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
+  | WhiteSpace n :: sl ->
+      Break n :: raw_analyze_notation_tokens sl
+
+let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn)
+
+let possible_notations ntn =
+  (* We collect the possible interpretations of a notation string depending on whether it is
+    in "x 'U' y" or "_ U _" format *)
+  let toks = split_notation_string ntn in
+  if List.exists (function String "_" -> true | _ -> false) toks then
+    (* Only "_ U _" format *)
+    [ntn]
+  else
+    let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in
+    if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
+
 let browse_notation strict ntn map =
-  let find ntn' =
+  let ntns = possible_notations ntn in
+  let find ntn' ntn =
     if String.contains ntn ' ' then String.equal ntn ntn'
     else
       let toks = decompose_notation_key ntn' in
@@ -940,7 +1018,7 @@ let browse_notation strict ntn map =
     String.Map.fold
       (fun scope_name sc ->
 	String.Map.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
-	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+          if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
   List.sort (fun x y -> String.compare (fst x) (fst y)) l
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 7d055571c8..a4c79d6d35 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -176,16 +176,20 @@ val scope_class_of_class : Classops.cl_typ -> scope_class
 (** Building notation key *)
 
 type symbol =
-  | Terminal of string
-  | NonTerminal of Id.t
-  | SProdList of Id.t * symbol list
-  | Break of int
+  | Terminal of string              (* an expression including symbols or a simply-quoted ident, e.g. "'U'" or "!" *)
+  | NonTerminal of Id.t             (* an identifier "x" *)
+  | SProdList of Id.t * symbol list (* an expression "x sep .. sep y", remembering x (or y) and sep *)
+  | Break of int                    (* a sequence of blanks > 1, e.g. "   " *)
 
 val symbol_eq : symbol -> symbol -> bool
 
+(** Make/decompose a notation of the form "_ U _" *)
 val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
+(** Decompose a notation of the form "a 'U' b" *)
+val decompose_raw_notation : string -> symbol list
+
 (** Prints scopes (expects a pure aconstr printer) *)
 val pr_scope_class : scope_class -> Pp.t
 val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 326d05cba6..c65f4785ef 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -42,9 +42,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
 | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
   Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) ->
   Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
-  (eq_notation_constr vars) u1 u2
+  (eq_notation_constr vars) u1 u2 && b1 == b2
 | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
   Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
   Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
@@ -101,13 +101,24 @@ let name_to_ident = function
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
+let product_of_cases_patterns patl =
+  List.fold_right (fun patl restl ->
+     List.flatten (List.map (fun p -> List.map (fun rest -> p::rest) restl) patl))
+    patl [[]]
+
 let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
   | PatVar na ->
-      let e',na' = g e na in e', DAst.make ?loc @@ PatVar na'
+      let e',disjpat,na' = g e na in
+      e', (match disjpat with
+      | None -> [DAst.make ?loc @@ PatVar na']
+      | Some ((_,disjpat),_) -> disjpat)
   | PatCstr (cstr,patl,na) ->
-      let e',na' = g e na in
+      let e',disjpat,na' = g e na in
+      if disjpat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern.");
       let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
-      e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
+      (* Distribute outwards the inner disjunctive patterns *)
+      let disjpatl' = product_of_cases_patterns patl' in
+      e', List.map (fun patl' -> DAst.make ?loc @@ PatCstr (cstr,patl',na')) disjpatl'
   )
 
 let subst_binder_type_vars l = function
@@ -136,6 +147,16 @@ let rec subst_glob_vars l gc = DAst.map (function
 
 let ldots_var = Id.of_string ".."
 
+let protect g e na =
+  let e',disjpat,na = g e na in
+  if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  e',na
+
+let apply_cases_pattern ?loc ((ids,disjpat),id) c =
+  let tm = DAst.make ?loc (GVar id) in
+  let eqns = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in
+  DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
@@ -146,46 +167,51 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       let inner  = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
       let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
       DAst.get (subst_glob_vars outerl it)
-  | NBinderList (x,y,iter,tail) ->
+  | NBinderList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
-      let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in
+      let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
       let inner  = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
-      let outerl = [(ldots_var,inner)] in
+      let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
       DAst.get (subst_glob_vars outerl it)
   | NLambda (na,ty,c) ->
-      let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
+      let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NProd (na,ty,c) ->
-      let e',na = g e na in GProd (na,Explicit,f e ty,f e' c)
+      let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c)
+      let e',disjpat,na = g e na in
+      (match disjpat with
+       | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
+       | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
-	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (Loc.tag ?loc (ind,nal')) in
-	let e',na' = g e' na in
-	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
+              let e',na' = protect g e' na in
+              e',na'::nal) nal (e',[]) in
+          e',Some (Loc.tag ?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 eqnl' = List.map (fun (patl,rhs) ->
-	let ((idl,e),patl) =
-	  List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
-	Loc.tag (idl,patl,f e rhs)) eqnl in
-      GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
+        let ((idl,e),patl) =
+          List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
+        let disjpatl = product_of_cases_patterns patl in
+        List.map (fun patl -> Loc.tag (idl,patl,f e rhs)) disjpatl) eqnl in
+      GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
-      let e',nal = List.fold_left_map g e nal in
-      let e'',na = g e na in
+      let e',nal = List.fold_left_map (protect g) e nal in
+      let e'',na = protect g e na in
       GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
   | NIf (c,(na,po),b1,b2) ->
-      let e',na = g e na in
+      let e',na = protect g e na in
       GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
-	  let e,na = g e na in
+      let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+          let e,na = protect g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      let e',idl = Array.fold_left_map (to_id g) e idl in
+      let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort x
@@ -195,13 +221,19 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
   in aux () x
 
 (******************************************************************************)
 (* Translating a glob_constr into a notation, interpreting recursive patterns *)
 
-let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
+type found_variables = {
+    vars : Id.t list;
+    recursive_term_vars : (Id.t * Id.t) list;
+    recursive_binders_vars : (Id.t * Id.t) list;
+  }
+
+let add_id r id = r := { !r with vars = id :: (!r).vars }
 let add_name r = function Anonymous -> () | Name id -> add_id r id
 
 let is_gvar id c = match DAst.get c with
@@ -245,13 +277,25 @@ let check_is_hole id t = match DAst.get t with GHole _ -> () | _ ->
    (strbrk "In recursive notation with binders, " ++ Id.print id ++
     strbrk " is expected to come without type.")
 
+let check_pair_matching ?loc x y x' y' revert revert' =
+  if not (Id.equal x x' && Id.equal y y' && revert = revert') then
+    let x,y = if revert then y,x else x,y in
+    let x',y' = if revert' then y',x' else x',y' in
+    (* This is a case where one would like to highlight two locations! *)
+    user_err ?loc
+      (strbrk "Found " ++ Id.print x ++ strbrk " matching " ++ Id.print y ++
+       strbrk " while " ++ Id.print x' ++ strbrk " matching " ++ Id.print y' ++
+       strbrk " was first found.")
+
 let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
 
+let mem_recursive_pair (x,y) l = List.mem_f (pair_equal Id.equal Id.equal) (x,y) l
+
 type recursive_pattern_kind =
-| RecursiveTerms of bool (* associativity *)
-| RecursiveBinders of glob_constr * glob_constr
+| RecursiveTerms of bool (* in reverse order *)
+| RecursiveBinders of bool (* in reverse order *)
 
-let compare_recursive_parts found f f' (iterator,subc) =
+let compare_recursive_parts recvars found f f' (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
   let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with
@@ -270,24 +314,41 @@ let compare_recursive_parts found f f' (iterator,subc) =
       List.for_all2eq aux l1 l2
     | _ -> mk_glob_constr_eq aux c1 c2
     end
-  | GVar x, GVar y when not (Id.equal x y) ->
+  | GVar x, GVar y
+        when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars ->
       (* We found the position where it differs *)
-      let lassoc = match !terminator with None -> false | Some _ -> true in
-      let x,y = if lassoc then y,x else x,y in
+      let revert = mem_recursive_pair (y,x) recvars in
+      let x,y = if revert then y,x else x,y in
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, RecursiveTerms lassoc) in
+        let () = diff := Some (x, y, RecursiveTerms revert) in
+        true
+      | Some (x', y', RecursiveTerms revert')
+      | Some (x', y', RecursiveBinders revert') ->
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
         true
-      | Some _ -> false
       end
   | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
-  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
+  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term)
+        when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars ->
       (* We found a binding position where it differs *)
+      check_is_hole x t_x;
+      check_is_hole y t_y;
+      let revert = mem_recursive_pair (y,x) recvars in
+      let x,y = if revert then y,x else x,y in
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in
+        let () = diff := Some (x, y, RecursiveBinders revert) in
         aux c term
-      | Some _ -> false
+      | Some (x', y', RecursiveBinders revert') ->
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
+        true
+      | Some (x', y', RecursiveTerms revert') ->
+        (* Recursive binders have precedence: they can be coerced to
+           terms but not reciprocally *)
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
+        let () = diff := Some (x, y, RecursiveBinders revert) in
+        true
       end
   | _ ->
       mk_glob_constr_eq aux c1 c2 in
@@ -296,46 +357,36 @@ let compare_recursive_parts found f f' (iterator,subc) =
     | None ->
 	let loc1 = loc_of_glob_constr iterator in
 	let loc2 = loc_of_glob_constr (Option.get !terminator) in
-	(* Here, we would need a loc made of several parts ... *)
-	user_err ?loc:(subtract_loc loc1 loc2)
+        (* Here, we would need a loc made of several parts ... *)
+        user_err ?loc:(subtract_loc loc1 loc2)
           (str "Both ends of the recursive pattern are the same.")
-    | Some (x,y,RecursiveTerms lassoc) ->
-        let toadd,x,y,lassoc =
-          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
-             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
-          then
-            None,x,y,lassoc
-          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
-                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
-          then
-            None,y,x,not lassoc
-          else
-            Some (x,y),x,y,lassoc in
-	let iterator =
-	  f' (if lassoc then iterator
-	      else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
-	(* found variables have been collected by compare_constr *)
-	found := (List.remove Id.equal y (pi1 !found),
-                  Option.fold_right (fun a l -> a::l) toadd (pi2 !found),
-                  pi3 !found);
-	NList (x,y,iterator,f (Option.get !terminator),lassoc)
-    | Some (x,y,RecursiveBinders (t_x,t_y)) ->
-	let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
-	(* found have been collected by compare_constr *)
-	found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found);
-	check_is_hole x t_x;
-	check_is_hole y t_y;
-	NBinderList (x,y,iterator,f (Option.get !terminator))
+    | Some (x,y,RecursiveTerms revert) ->
+        (* By arbitrary convention, we use the second variable of the pair
+           as the place-holder for the iterator *)
+        let iterator =
+          f' (if revert then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
+        (* found variables have been collected by compare_constr *)
+        found := { !found with vars = List.remove Id.equal y (!found).vars;
+                               recursive_term_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars };
+        NList (x,y,iterator,f (Option.get !terminator),revert)
+    | Some (x,y,RecursiveBinders revert) ->
+        let iterator =
+          f' (if revert then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
+        (* found have been collected by compare_constr *)
+        found := { !found with vars = List.remove Id.equal y (!found).vars;
+                               recursive_binders_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars };
+        NBinderList (x,y,iterator,f (Option.get !terminator),revert)
   else
     raise Not_found
 
-let notation_constr_and_vars_of_glob_constr a =
-  let found = ref ([],[],[]) in
+let notation_constr_and_vars_of_glob_constr recvars a =
+  let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in
   let has_ltac = ref false in
+  (* Turn a glob_constr into a notation_constr by first trying to find a recursive pattern *)
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
-    try compare_recursive_parts found aux aux' (split_at_recursive_part c)
+    try compare_recursive_parts recvars found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
     match DAst.get c with
@@ -395,8 +446,9 @@ let notation_constr_and_vars_of_glob_constr a =
   (* Side effect *)
   t, !found, !has_ltac
 
-let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
-  let injective = ref true in
+let check_variables_and_reversibility nenv
+  { vars = found; recursive_term_vars = foundrec; recursive_binders_vars = foundrecbinding } =
+  let injective = ref [] in
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
   let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
@@ -419,33 +471,36 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
 	user_err Pp.(str
           (Id.to_string x ^
           " should not be bound in a recursive pattern of the right-hand side."))
-      else injective := false
+      else injective := x :: !injective
   in
   let check_pair s x y where =
-    if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
+    if not (mem_recursive_pair (x,y) where) then
       user_err  (strbrk "in the right-hand side, " ++ Id.print x ++
 	str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
   let check_type x typ =
     match typ with
-    | NtnInternTypeConstr ->
+    | NtnInternTypeAny ->
 	begin
 	  try check_pair "term" x (Id.Map.find x recvars) foundrec
 	  with Not_found -> check_bound x
 	end
-    | NtnInternTypeBinder ->
+    | NtnInternTypeOnlyBinder ->
 	begin
 	  try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding
 	  with Not_found -> check_bound x
-	end
-    | NtnInternTypeIdent -> check_bound x in
+        end in
   Id.Map.iter check_type vars;
-  !injective
+  List.rev !injective
 
 let notation_constr_of_glob_constr nenv a =
-  let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
+  let recvars = Id.Map.bindings nenv.ninterp_rec_vars in
+  let a, found, has_ltac = notation_constr_and_vars_of_glob_constr recvars a in
   let injective = check_variables_and_reversibility nenv found in
-  a, not has_ltac && injective
+  let status = if has_ltac then HasLtac else match injective with
+  | [] -> APrioriReversible
+  | l -> NonInjective l in
+  a, status
 
 (**********************************************************************)
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
@@ -501,11 +556,11 @@ let rec subst_notation_constr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  NProd (n,r1',r2')
 
-  | NBinderList (id1,id2,r1,r2) ->
+  | NBinderList (id1,id2,r1,r2,b) ->
       let r1' = subst_notation_constr subst bound r1
       and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  NBinderList (id1,id2,r1',r2')
+          NBinderList (id1,id2,r1',r2',b)
 
   | NLetIn (n,r1,t,r2) ->
       let r1' = subst_notation_constr subst bound r1 in
@@ -616,8 +671,20 @@ let is_term_meta id metas =
   try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
   with Not_found -> false
 
+let is_onlybinding_strict_meta id metas =
+  try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false
+  with Not_found -> false
+
 let is_onlybinding_meta id metas =
-  try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false
+  try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
+  with Not_found -> false
+
+let is_onlybinding_pattern_like_meta isvar id metas =
+  try match Id.List.assoc id metas with
+      | _,NtnTypeBinder (NtnBinderParsedAsConstr
+                           (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+      | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+      | _ -> false
   with Not_found -> false
 
 let is_bindinglist_meta id metas =
@@ -636,7 +703,7 @@ let alpha_rename alpmetas v =
   if alpmetas == [] then v
   else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
 
-let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
+let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
   (* Check that no capture of binding variables occur *)
   (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
      with an actual term "fun z => ... z ..." when "x" is not bound in the
@@ -664,19 +731,49 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
      refinement *)
   let v = alpha_rename alpmetas v in
   (* TODO: handle the case of multiple occs in different scopes *)
-  ((var,v)::terms,onlybinders,termlists,binderlists)
+  ((var,v)::terms,termlists,binders,binderlists)
 
-let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl =
+let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl =
   if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
   let vl = List.map (alpha_rename alpmetas) vl in
-  (terms,onlybinders,(var,vl)::termlists,binderlists)
+  (terms,(var,vl)::termlists,binders,binderlists)
 
-let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
+let add_binding_env alp (terms,termlists,binders,binderlists) var v =
   (* TODO: handle the case of multiple occs in different scopes *)
-  (terms,(var,v)::onlybinders,termlists,binderlists)
+  (terms,termlists,(var,v)::binders,binderlists)
 
-let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
-  (terms,onlybinders,termlists,(x,bl)::binderlists)
+let add_bindinglist_env (terms,termlists,binders,binderlists) x bl =
+  (terms,termlists,binders,(x,bl)::binderlists)
+
+let rec map_cases_pattern_name_left f = DAst.map (function
+  | PatVar na -> PatVar (f na)
+  | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
+  )
+
+let rec fold_cases_pattern_eq f x p p' =
+  let loc = p.CAst.loc in
+  match DAst.get p, DAst.get p' with
+  | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
+  | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
+     let x,l = fold_cases_pattern_list_eq f x l l' in
+     let x,na = f x na na' in
+     x, DAst.make ?loc @@ PatCstr (c,l,na)
+  | _ -> failwith "Not equal"
+
+and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
+  | [], [] -> x, []
+  | p::pl, p'::pl' ->
+     let x, p = fold_cases_pattern_eq f x p p' in
+     let x, pl = fold_cases_pattern_list_eq f x pl pl' in
+     x, p :: pl
+  | _ -> assert false
+
+let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
+| PatVar na1, PatVar na2 -> Name.equal na1 na2
+| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
+  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+  Name.equal na1 na2
+| _ -> false
 
 let rec pat_binder_of_term t = DAst.map (function
   | GVar id -> PatVar (Name id)
@@ -691,39 +788,111 @@ let rec pat_binder_of_term t = DAst.map (function
   | _ -> raise No_match
   ) t
 
-let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+let unify_name_upto alp na na' =
+  match na, na' with
+  | Anonymous, na' -> alp, na'
+  | na, Anonymous -> alp, na
+  | Name id, Name id' ->
+     if Id.equal id id' then alp, na'
+     else (fst alp,(id,id')::snd alp), na'
+
+let unify_pat_upto alp p p' =
+  try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match
+
+let unify_term alp v v' =
+  match DAst.get v, DAst.get v' with
+  | GHole _, _ -> v'
+  | _, GHole _ -> v
+  | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match
+
+let unify_opt_term alp v v' =
+  match v, v' with
+  | Some t, Some t' -> Some (unify_term alp t t')
+  | (Some _ as x), None | None, (Some _ as x) -> x
+  | None, None -> None
+
+let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match
+
+let unify_binder_upto alp b b' =
+  let loc, loc' = CAst.(b.loc, b'.loc) in
+  match DAst.get b, DAst.get b' with
+  | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
+     let alp, na = unify_name_upto alp na na' in
+     alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+  | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
+     let alp, na = unify_name_upto alp na na' in
+     alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+  | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' ->
+     let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
+     alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+  | _ -> raise No_match
+
+let rec unify_terms alp vl vl' =
+  match vl, vl' with
+  | [], [] -> []
+  | v :: vl, v' :: vl' -> unify_term alp v v' :: unify_terms alp vl vl'
+  | _ -> raise No_match
+
+let rec unify_binders_upto alp bl bl' =
+  match bl, bl' with
+  | [], [] -> alp, []
+  | b :: bl, b' :: bl' ->
+     let alp,b = unify_binder_upto alp b b' in
+     let alp,bl = unify_binders_upto alp bl bl' in
+     alp, b :: bl
+  | _ -> raise No_match
+
+let unify_id alp id na' =
+  match na' with
+  | Anonymous -> Name (rename_var (snd alp) id)
+  | Name id' ->
+     if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match
+
+let unify_pat alp p p' =
+  if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
+  else raise No_match
+
+let unify_term_binder alp c = DAst.(map (fun b' ->
+  match DAst.get c, b' with
+  | GVar id, GLocalAssum (na', bk', t') ->
+     GLocalAssum (unify_id alp id na', bk', t')
+  | _, GLocalPattern (([p'],ids), id, bk', t') ->
+     let p = pat_binder_of_term c in
+     GLocalPattern (([unify_pat alp p p'],ids), id, bk', t')
+  | _ -> raise No_match))
+
+let rec unify_terms_binders alp cl bl' =
+  match cl, bl' with
+  | [], [] -> []
+  | c :: cl, b' :: bl' ->
+     begin match DAst.get b' with
+     | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl'
+     | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl'
+     end
+  | _ -> raise No_match
+
+let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v =
   try
+    (* If already bound to a term, unify with the new term *)
     let v' = Id.List.assoc var terms in
-    match DAst.get v, DAst.get v' with
-    | GHole _, _ -> sigma
-    | _, GHole _ ->
-        let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
-        add_env alp sigma var v
-    | _, _ ->
-        if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma
-        else raise No_match
+    let v'' = unify_term alp v v' in
+    if v'' == v' then sigma else
+      let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in
+      add_env alp sigma var v
   with Not_found -> add_env alp sigma var v
 
-let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
+let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl =
   try
+    (* If already bound to a list of term, unify with the new terms *)
     let vl' = Id.List.assoc var termlists in
-    let unify_term v v' =
-      match DAst.get v, DAst.get v' with
-      | GHole _, _ -> v'
-      | _, GHole _ -> v
-      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
-    let rec unify vl vl' =
-      match vl, vl' with
-      | [], [] -> []
-      | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl'
-      | _ -> raise No_match in
-    let vl = unify vl vl' in
-    let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
+    let vl = unify_terms alp vl vl' in
+    let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in
     add_termlist_env alp sigma var vl
   with Not_found -> add_termlist_env alp sigma var vl
 
-let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id =
   try
+    (* If already bound to a term, unify the binder and the term *)
     match DAst.get (Id.List.assoc var terms) with
     | GVar id' ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
@@ -735,142 +904,49 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
-let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+let force_cases_pattern c =
+  DAst.make ?loc:c.CAst.loc (DAst.get c)
+
+let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
+  let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
   try
-    let v' = Id.List.assoc var onlybinders in
-    match v' with
-    | Anonymous ->
-        (* Should not occur, since the term has to be bound upwards *)
-        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
-        add_binding_env alp sigma var (Name id)
-    | Name id' ->
-        if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match
-  with Not_found -> add_binding_env alp sigma var (Name id)
-
-let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+    (* If already bound to a binder, unify the term and the binder *)
+    let patl' = Id.List.assoc var binders in
+    let patl'' = List.map2 (unify_pat alp) [pat] patl' in
+    if patl' == patl'' then sigma
+    else
+      let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+      add_binding_env alp sigma var patl''
+  with Not_found -> add_binding_env alp sigma var [pat]
+
+let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat =
   try
-    let v' = Id.List.assoc var onlybinders in
-    match v, v' with
-    | Anonymous, _ -> alp, sigma
-    | _, Anonymous ->
-        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
-        alp, add_binding_env alp sigma var v
-    | Name id1, Name id2 ->
-        if Id.equal id1 id2 then alp,sigma
-        else (fst alp,(id1,id2)::snd alp),sigma
-  with Not_found -> alp, add_binding_env alp sigma var v
-
-let rec map_cases_pattern_name_left f = DAst.map (function
-  | PatVar na -> PatVar (f na)
-  | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
-  )
-
-let rec fold_cases_pattern_eq f x p p' =
-  let loc = p.CAst.loc in
-  match DAst.get p, DAst.get p' with
-  | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
-  | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
-     let x,l = fold_cases_pattern_list_eq f x l l' in
-     let x,na = f x na na' in
-     x, DAst.make ?loc @@ PatCstr (c,l,na)
-  | _ -> failwith "Not equal"
-
-and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
-  | [], [] -> x, []
-  | p::pl, p'::pl' ->
-     let x, p = fold_cases_pattern_eq f x p p' in
-     let x, pl = fold_cases_pattern_list_eq f x pl pl' in
-     x, p :: pl
-  | _ -> assert false
-
-let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
-| PatVar na1, PatVar na2 -> Name.equal na1 na2
-| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
-  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
-  Name.equal na1 na2
-| _ -> false
-
-let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
+    (* If already bound to a binder possibly *)
+    (* generating an alpha-renaming from unifying the new binder *)
+    let disjpat' = Id.List.assoc var binders in
+    let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
+    let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+    alp, add_binding_env alp sigma var disjpat
+  with Not_found -> alp, add_binding_env alp sigma var disjpat
+
+let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
   let bl = List.rev bl in
   try
+    (* If already bound to a list of binders possibly *)
+    (* generating an alpha-renaming from unifying the new binders *)
     let bl' = Id.List.assoc var binderlists in
-    let unify_name alp na na' =
-      match na, na' with
-      | Anonymous, na' -> alp, na'
-      | na, Anonymous -> alp, na
-      | Name id, Name id' ->
-         if Id.equal id id' then alp, na'
-         else (fst alp,(id,id')::snd alp), na' in
-    let unify_pat alp p p' =
-      try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
-    let unify_term alp v v' =
-      match DAst.get v, DAst.get v' with
-      | GHole _, _ -> v'
-      | _, GHole _ -> v
-      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
-    let unify_opt_term alp v v' =
-      match v, v' with
-      | Some t, Some t' -> Some (unify_term alp t t')
-      | (Some _ as x), None | None, (Some _ as x) -> x
-      | None, None -> None in
-    let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
-    let unify_binder alp b b' =
-      let loc, loc' = CAst.(b.loc, b'.loc) in
-      match DAst.get b, DAst.get b' with
-      | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
-         let alp, na = unify_name alp na na' in
-         alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
-      | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
-         let alp, na = unify_name alp na na' in
-         alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
-      | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
-         let alp, p = unify_pat alp p p' in
-         alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
-      | _ -> raise No_match in
-    let rec unify alp bl bl' =
-    match bl, bl' with
-    | [], [] -> alp, []
-    | b :: bl, b' :: bl' ->
-       let alp,b = unify_binder alp b b' in
-       let alp,bl = unify alp bl bl' in
-       alp, b :: bl
-    | _ -> raise No_match in
-    let alp, bl = unify alp bl bl' in
-    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+    let alp, bl = unify_binders_upto alp bl bl' in
+    let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
     alp, add_bindinglist_env sigma var bl
   with Not_found ->
     alp, add_bindinglist_env sigma var bl
 
-let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl =
+let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl =
   try
+    (* If already bound to a list of binders, unify the terms and binders *)
     let bl' = Id.List.assoc var binderlists in
-    let unify_id id na' =
-      match na' with
-      | Anonymous -> Name (rename_var (snd alp) id)
-      | Name id' ->
-         if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
-    let unify_pat p p' =
-      if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
-      else raise No_match in
-    let unify_term_binder c = DAst.(map (fun b' ->
-      match DAst.get c, b' with
-      | GVar id, GLocalAssum (na', bk', t') ->
-         GLocalAssum (unify_id id na', bk', t')
-      | _, GLocalPattern ((p',ids), id, bk', t') ->
-         let p = pat_binder_of_term c in
-         GLocalPattern ((unify_pat p p',ids), id, bk', t')
-      | _ -> raise No_match )) in
-    let rec unify cl bl' =
-    match cl, bl' with
-    | [], [] -> []
-    | c :: cl, b' :: bl' ->
-      begin match DAst.get b' with
-      | GLocalDef ( _, _, _, t) -> unify cl bl'
-      | _ -> unify_term_binder c b' :: unify cl bl'
-      end
-    | _ -> raise No_match in
-    let bl = unify cl bl' in
-    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+    let bl = unify_terms_binders alp cl bl' in
+    let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
     add_bindinglist_env sigma var bl
   with Not_found ->
     anomaly (str "There should be a binder list bindings this list of terms.")
@@ -894,8 +970,10 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+  | (na1,Name id2) when is_onlybinding_strict_meta id2 metas ->
+      raise No_match
   | (na1,Name id2) when is_onlybinding_meta id2 metas ->
-      bind_binding_env alp sigma id2 na1
+      bind_binding_env alp sigma id2 [DAst.make (PatVar na1)]
   | (Name id1,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs and hence reason up to *)
       (* alpha-conversion for the given occurrence of the name (see #4592)) *)
@@ -907,54 +985,42 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern_binders metas acc pat1 pat2 =
+let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 =
   match DAst.get pat1, DAst.get pat2 with
+  | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas ->
+      bind_binding_env alp sigma id2 [pat1]
+  | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
+      bind_binding_env alp sigma id2 [pat1]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
+  | _, PatVar Anonymous when allow_catchall -> acc
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
-      List.fold_left2 (match_cases_pattern_binders metas)
-	(match_names metas acc na1 na2) patl1 patl2
+      List.fold_left2 (match_cases_pattern_binders false metas)
+        (match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
-let glue_letin_with_decls = true
-
-let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function
-  | GLambda (na,bk,t,b) as b0 ->
-    begin match na, DAst.get b with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when islambda && is_gvar p e && not (occur_glob_constr p b) ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
-    | _, _ when islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
-    | _ -> (decls, DAst.make ?loc b0)
-    end
-  | GProd (na,bk,t,b) as b0 ->
-    begin match na, DAst.get b with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
-      when not islambda && is_gvar p e && not (occur_glob_constr p b) ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
-    | Name _, _ when not islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
-    | _ -> (decls, DAst.make ?loc b0)
-    end
-  | GLetIn (na,c,t,b) when glue_letin_with_decls ->
-      match_iterated_binders islambda
-	((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
-  | b -> (decls, DAst.make ?loc b)
-  )) bi
-
-let remove_sigma x (terms,onlybinders,termlists,binderlists) =
-  (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
+let remove_sigma x (terms,termlists,binders,binderlists) =
+  (Id.List.remove_assoc x terms,termlists,binders,binderlists)
 
-let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
-  (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists)
+let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
+  (terms,termlists,binders,Id.List.remove_assoc x binderlists)
 
 let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
 let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
 
-let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
-  let rec aux sigma bl rest =
+(* This tells if letins in the middle of binders should be included in
+   the sequence of binders *)
+let glue_inner_letin_with_decls = true
+
+(* This tells if trailing letins (with no further proper binders)
+   should be included in sequence of binders *)
+let glue_trailing_letin_with_decls = false
+
+exception OnlyTrailingLetIns
+
+let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
+  let rec aux trailing_letins sigma bl rest =
     try
       let metas = add_ldots_var (add_meta_bindinglist y metas) in
       let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
@@ -963,16 +1029,32 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
         match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
       in
       let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
-      aux sigma (b::bl) rest
-    with No_match when not (List.is_empty bl) ->
-      bl, rest, sigma in
-  let bl,rest,sigma = aux sigma [] rest in
+      (* In case y is bound not only to a binder but also to a term *)
+      let sigma = remove_sigma y sigma in
+      aux false sigma (b::bl) rest
+    with No_match ->
+    match DAst.get rest with
+    | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls ->
+       let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in
+       (* collect let-in *)
+       (try aux true sigma (b::bl) rest'
+        with OnlyTrailingLetIns
+             when not (trailing_letins && not glue_trailing_letin_with_decls) ->
+         (* renounce to take into account trailing let-ins *)
+         if not (List.is_empty bl) then bl, rest, sigma else raise No_match)
+    | _ ->
+       if trailing_letins && not glue_trailing_letin_with_decls then
+         (* Backtrack to when we tried to glue letins *)
+         raise OnlyTrailingLetIns;
+       if not (List.is_empty bl) then bl, rest, sigma else raise No_match in
+  let bl,rest,sigma = aux false sigma [] rest in
+  let bl = if revert then List.rev bl else bl in
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
   match_fun alp metas sigma rest termin
 
 let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
 
-let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma acc rest =
     try
       let metas = add_ldots_var (add_meta_term y metas) in
@@ -983,12 +1065,12 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
-  let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  let l = if lassoc then l else List.rev l in
+  let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
+  let l = if revert then l else List.rev l in
   if is_bindinglist_meta x metas then
     (* This is a recursive pattern for both bindings and terms; it is *)
     (* registered for binders *)
-    bind_bindinglist_as_term_env alp sigma x l
+    bind_bindinglist_as_termlist_env alp sigma x l
   else
     bind_termlist_env alp sigma x l
 
@@ -1023,72 +1105,19 @@ let rec match_ inner u alp metas sigma a1 a2 =
   match DAst.get a1, a2 with
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
-  | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+  | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
+  | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)
-  | r1, NList (x,y,iter,termin,lassoc) ->
-      match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
-
-  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
-    begin match na1, DAst.get b1, iter with
-    (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _)
-      when is_gvar p e && not (occur_glob_constr p b1) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-    | _, _, NLambda (Name _,_,_) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
-      (* TODO: address the possibility that termin is a Lambda itself *)
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: general case *)
-    | _, _, _ ->
-      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
-    end
-
-  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
-    (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-    begin match na1, DAst.get b1, iter, termin with
-    | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _
-      when is_gvar p e && not (occur_glob_constr p b1) ->
-      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    | _, _,  NProd (Name _,_,_), _ when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
-      (* TODO: address the possibility that termin is a Prod itself *)
-      let alp,sigma = bind_bindinglist_env alp sigma x decls in
-      match_in u alp metas sigma b termin
-    (* Matching recursive notations for binders: general case *)
-    | _, _, _, _ ->
-      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
-    end
+  | r1, NList (x,y,iter,termin,revert) ->
+      match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert
 
   (* Matching recursive notations for binders: general case *)
-  | _r, NBinderList (x,y,iter,termin) ->
-       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
-
-  (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
-    begin match na1, DAst.get b1, na2 with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-      when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _, _, Name id when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _ ->
-      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-    end
-
-  | GProd (na,bk,t,b1), NProd (Name id,_,b2)
-      when is_bindinglist_meta id metas && na != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in
-      match_in u alp metas sigma b1 b2
+  | _r, NBinderList (x,y,iter,termin,revert) ->
+      match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
@@ -1104,8 +1133,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
-  | GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
-     match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+  | 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
+  | 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
   | 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
@@ -1113,9 +1144,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
      match_binders u alp metas na1 na2
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
-      when sty1 == sty2
-	 && Int.equal (List.length tml1) (List.length tml2)
-	 && Int.equal (List.length eqnl1) (List.length eqnl2) ->
+      when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) ->
       let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in
       let sigma =
@@ -1125,7 +1154,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let sigma = List.fold_left2
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
-      List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
+      (* Try two different strategies for matching clauses *)
+      (try
+        List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
+      with
+        No_match ->
+        List.fold_left2_set No_match (match_disjunctive_equations u alp metas) sigma
+           (Detyping.factorize_eqns eqnl1)
+           (List.map (fun (patl,rhs) -> ([patl],rhs)) eqnl2))
   | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when Int.equal (List.length nal1) (List.length nal2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
@@ -1191,44 +1227,83 @@ and match_in u = match_ true u
 and match_hd u = match_ false u
 
 and match_binders u alp metas na1 na2 sigma b1 b2 =
+  (* Match binders which cannot be substituted by a pattern *)
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_in u alp metas sigma b1 b2
 
-and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
+and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
+  (* Match binders which can be substituted by a pattern *)
+  let store, get = set_temporary_memory () in
+  match na1, DAst.get b1, na2 with
+  (* Matching individual binders as part of a recursive pattern *)
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+       when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
+    (match get () with
+     | [(_,(ids,disj_of_patl,b1))] ->
+     let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
+     let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
+     let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((disjpat,ids),p,bk,t)] in
+     match_in u alp metas sigma b1 b2
+     | _ -> assert false)
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+       when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
+    (match get () with
+     | [(_,(ids,disj_of_patl,b1))] ->
+     let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
+     let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
+     let alp,sigma = bind_binding_env alp sigma id disjpat in
+     match_in u alp metas sigma b1 b2
+     | _ -> assert false)
+  | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
+      match_in u alp metas sigma b1 b2
+  | _, _, _ ->
+     let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
+     match_in u alp metas sigma b1 b2
+
+and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
+  let allow_catchall = (rest2 = [] && ids = []) in
   let (alp,sigma) =
-    List.fold_left2 (match_cases_pattern_binders metas)
+    List.fold_left2 (match_cases_pattern_binders allow_catchall metas)
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let term_of_binder bi = DAst.make @@ match bi with
-  | Name id -> GVar id
-  | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ =
+  (* patl1 and patl2 have the same length because they respectively
+     correspond to some tml1 and tml2 that have the same length *)
+  let (alp,sigma) =
+    List.fold_left2_set No_match
+      (fun alp_sigma patl1 patl2 _ _ ->
+        List.fold_left2 (match_cases_pattern_binders false metas) alp_sigma patl1 patl2)
+      (alp,sigma) disjpatl1 disjpatl2 in
+  match_in u alp metas sigma rhs1 rhs2
 
 let match_notation_constr u c (metas,pat) =
-  let terms,binders,termlists,binderlists =
+  let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
-  (* Reorder canonically the substitution *)
-  let find_binder x =
-    try term_of_binder (Id.List.assoc x binders)
-    with Not_found ->
-      (* Happens for binders bound to Anonymous *)
-      (* Find a better way to propagate Anonymous... *)
-      DAst.make @@GVar x in
-  List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
+  (* Turning substitution based on binding/constr distinction into a
+     substitution based on entry productions *)
+  List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') ->
     match typ with
     | NtnTypeConstr ->
       let term = try Id.List.assoc x terms with Not_found -> raise No_match in
-       ((term, scl)::terms',termlists',binders')
-    | NtnTypeOnlyBinder ->
-       ((find_binder x, scl)::terms',termlists',binders')
+       ((term, scl)::terms',termlists',binders',binderlists')
+    | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
+       (match Id.List.assoc x binders with
+        | [pat] ->
+          let v = glob_constr_of_cases_pattern pat in
+          ((v,scl)::terms',termlists',binders',binderlists')
+        | _ -> raise No_match)
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+       (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
-       (terms',(Id.List.assoc x termlists,scl)::termlists',binders')
+       (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
     | NtnTypeBinderList ->
       let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in
-       (terms',termlists',(bl, scl)::binders'))
-    metas ([],[],[])
+       (terms',termlists',binders',(bl, scl)::binderlists'))
+    metas ([],[],[],[])
 
 (* Matching cases pattern *)
 
@@ -1240,7 +1315,7 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::terms,x,termlists,y
 
-let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
   let rec aux sigma acc rest =
     try
       let metas = add_ldots_var (add_meta_term y metas) in
@@ -1251,10 +1326,10 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
-  let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
+  let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
+  (terms,(x,if revert then l else List.rev l)::termlists,binders,binderlists)
 
-let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
+let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
@@ -1270,10 +1345,10 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
 	raise No_match
       else
 	let l1',more_args = Util.List.chop le2 l1 in
-	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
-  | r1, NList (x,y,iter,termin,lassoc) ->
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+  | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-	metas (terms,(),termlists,()) a1 x y iter termin lassoc),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
@@ -1300,15 +1375,15 @@ let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
       | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
-      | NtnTypeOnlyBinder -> assert false
+      | NtnTypeBinder _ -> assert false
       | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
       | NtnTypeBinderList -> assert false)
     metas ([],[])
 
 let match_notation_constr_cases_pattern c (metas,pat) =
-  let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in
+  let (terms,termlists,(),()),more_args = match_cases_pattern metas ([],[],(),()) c pat in
   reorder_canonically_substitution terms termlists metas, more_args
 
 let match_notation_constr_ind_pattern ind args (metas,pat) =
-  let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in
+  let (terms,termlists,(),()),more_args = match_ind_pattern metas ([],[],(),()) ind args pat in
   reorder_canonically_substitution terms termlists metas, more_args
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 0904a4ea3e..746f52e485 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,12 +29,15 @@ val ldots_var : Id.t
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr * reversibility_flag
+  glob_constr -> notation_constr * reversibility_status
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
+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 * Name.t) ->
+  ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
   ('a -> notation_constr -> glob_constr) ->
   'a -> notation_constr -> glob_constr
 
@@ -49,6 +52,7 @@ exception No_match
 
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
       ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
+      ('a cases_pattern_disjunction_g * subscopes) list *
       ('a extended_glob_local_binder_g list * subscopes) list
 
 val match_notation_constr_cases_pattern :
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index ce19dd8a92..606196fcd1 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -33,6 +33,7 @@ let ppcmd_of_cut = function
 
 type unparsing =
   | UnpMetaVar of int * parenRelation
+  | UnpBinderMetaVar of int * parenRelation
   | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 7b62a2074b..77823e32a5 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -26,6 +26,7 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 type unparsing =
   | UnpMetaVar of int * parenRelation
+  | UnpBinderMetaVar of int * parenRelation
   | UnpListMetaVar of int * parenRelation * unparsing list
   | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 22c5a2f5e5..04710282f5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -71,7 +71,7 @@ let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+  | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | _ -> Oth, None