Extension of the recursive notations mechanism

- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7

34 files changed, 1194 insertions, 552 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 6b471ec39..f5c3dfcaf 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -474,6 +474,8 @@ Locate "'exists' _ , _".
   & $|$ & {\tt right associativity} \\
   & $|$ & {\tt no associativity} \\
   & $|$ & {\ident} {\tt ident} \\
+  & $|$ & {\ident} {\tt binder} \\
+  & $|$ & {\ident} {\tt closed binder} \\
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
   & $|$ & {\tt only parsing} \\
@@ -485,69 +487,7 @@ Locate "'exists' _ , _".
 \label{notation-syntax}
 \end{figure}
 
-\subsection{Notations with recursive patterns}
-
-An experimental mechanism is provided for declaring elementary
-notations including recursive patterns. The basic syntax is
-
-\begin{coq_eval}
-Require Import List.
-\end{coq_eval}
-
-\begin{coq_example*}
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
-\end{coq_example*}
-
-On the right-hand-side, an extra construction of the form {\tt ..} ($f$
-$t_1$ $\ldots$ $t_n$) {\tt ..} can be used. Notice that {\tt ..} is part of
-the {\Coq} syntax while $\ldots$ is just a meta-notation of this
-manual to denote a sequence of terms of arbitrary size.
-
-This extra construction enclosed within {\tt ..}, let's call it $t$,
-must be one of the argument of an applicative term of the form {\tt
-($f$ $u_1$ $\ldots$ $u_n$)}. The sequences $t_1$ $\ldots$ $t_n$ and
-$u_1$ $\ldots$ $u_n$ must coincide everywhere but in two places. In
-one place, say the terms of indice $i$, we must have $u_i = t$. In the
-other place, say the terms of indice $j$, both $u_j$ and $t_j$ must be
-variables, say $x$ and $y$ which are bound by the notation string on
-the left-hand-side of the declaration. The variables $x$ and $y$ in
-the string must occur in a substring of the form "$x$ $s$ {\tt ..} $s$
-$y$" where {\tt ..} is part of the syntax and $s$ is two times the
-same sequence of terminal symbols (i.e. symbols which are not
-variables).
-
-These invariants must be satisfied in order the notation to be
-correct.  The term $t_i$ is the {\em terminating} expression of
-the notation and the pattern {\tt ($f$ $u_1$ $\ldots$ $u_{i-1}$ {\rm [I]}
-$u_{i+1}$ $\ldots$ $u_{j-1}$ {\rm [E]} $u_{j+1}$ $\ldots$ $u_{n}$)} is the
-{\em iterating pattern}. The hole [I] is the {\em iterative} place
-and the hole [E] is the {\em enumerating} place. Remark that if $j<i$, the
-iterative place comes after the enumerating place accordingly.
-
-The notation parses sequences of tokens such that the subpart "$x$ $s$
-{\tt ..} $s$ $y$" parses any number of time (but at least one time) a
-sequence of expressions separated by the sequence of tokens $s$. The
-parsing phase produces a list of expressions which
-are used to fill in order the holes [E] of the iterating pattern
-which is nested as many time as the length of the list, the hole [I]
-being the nesting point. In the innermost occurrence of the nested
-iterating pattern, the hole [I] is finally filled with the terminating
-expression.
-
-In the example above, $f$ is {\tt cons}, $n=3$ (because {\tt cons} has
-a hidden implicit argument!), $i=3$ and $j=2$. The {\em terminating}
-expression is {\tt nil} and the {\em iterating pattern} is {\tt cons
-{\rm [E] [I]}}. Finally, the sequence $s$ is made of the single token
-``{\tt ;}''. Here is another example.
-\begin{coq_example*}
-Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
-\end{coq_example*}
-
-Notations with recursive patterns can be reserved like standard
-notations, they can also be declared within interpretation scopes (see
-section \ref{scopes}).
-
-\subsection{Notations and binders}
+\subsection{Notations and simple binders}
 
 Notations can be defined for binders as in the example:
 
@@ -592,6 +532,105 @@ parsed at level 99 to be factorized with the notation
 However, even if parsed as a term, this term must at the end be effectively 
 a single identifier.
 
+\subsection{Notations with recursive patterns}
+\label{RecursiveNotations}
+
+A mechanism is provided for declaring elementary notations with
+recursive patterns. The basic example is:
+
+\begin{coq_example*}
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
+\end{coq_example*}
+
+On the right-hand side, an extra construction of the form {\tt ..} $t$
+{\tt ..} can be used. Notice that {\tt ..} is part of the {\Coq}
+syntax and it must not be confused with the three-dots notation
+$\ldots$ used in this manual to denote a sequence of arbitrary size.
+
+On the left-hand side, the part ``$x$ $s$ {\tt ..} $s$ $y$'' of the
+notation parses any number of time (but at least one time) a sequence
+of expressions separated by the sequence of tokens $s$ (in the
+example, $s$ is just ``{\tt ;}'').
+
+In the right-hand side, the term enclosed within {\tt ..} must be a
+pattern with two holes of the form $\phi([~]_E,[~]_I)$ where the first
+hole is occupied either by $x$ or by $y$ and the second hole is
+occupied by an arbitrary term $t$ called the {\it terminating}
+expression of the recursive notation. The subterm {\tt ..} $\phi(x,t)$
+{\tt ..} (or {\tt ..} $\phi(y,t)$ {\tt ..})  must itself occur at
+second position of the same pattern where the first hole is occupied
+by the other variable, $y$ or $x$. Otherwise said, the right-hand side
+must contain a subterm of the form either $\phi(x,${\tt ..}
+$\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..}  $\phi(x,t)$ {\tt ..}$)$.
+The pattern $\phi$ is the {\em iterator} of the recursive notation
+and, of course, the name $x$ and $y$ can be chosen arbitrarily.
+
+The parsing phase produces a list of expressions which are used to
+fill in order the first hole of the iterating pattern which is
+repeatedly nested as many times as the length of the list, the second
+hole being the nesting point. In the innermost occurrence of the
+nested iterating pattern, the second hole is finally filled with the
+terminating expression.
+
+In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons
+  $[~]_E$ $[~]_I$} and the terminating expression is {\tt nil}. Here are
+other examples:
+\begin{coq_example*}
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
+Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
+  (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
+        (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
+  (t at level 39).
+\end{coq_example*}
+
+Notations with recursive patterns can be reserved like standard
+notations, they can also be declared within interpretation scopes (see
+section \ref{scopes}).
+
+\subsection{Notations with recursive patterns involving binders}
+
+Recursive notations can also be used with binders. The basic example is:
+
+\begin{coq_example*}
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  (at level 200, x binder, y binder, right associativity).
+\end{coq_example*}
+
+The principle is the same as in Section~\ref{RecursiveNotations}
+except that in the iterator $\phi([~]_E,[~]_I)$, the first hole is a
+placeholder occurring at the position of the binding variable of a {\tt
+  fun} or a {\tt forall}.
+
+To specify that the part ``$x$ {\tt ..} $y$'' of the notation
+parses a sequence of binders, $x$ and $y$ must be marked as {\tt
+  binder} in the list of modifiers of the notation.  Then, the list of
+binders produced at the parsing phase are used to fill in the first
+hole of the iterating pattern which is repeatedly nested as many times
+as the number of binders generated. If ever the generalization
+operator {\tt `} (see Section~\ref{implicit-generalization}) is used
+in the binding list, the added binders are taken into account too.
+
+Binders parsing exist in two flavors. If $x$ and $y$ are marked as
+{\tt binder}, then a sequence such as {\tt a b c : T} will be accepted
+and interpreted as the sequence of binders {\tt (a:T) (b:T)
+  (c:T)}. For instance, in the notation above, the syntax {\tt exists
+  a b : nat, a = b} is provided.
+
+The variables $x$ and $y$ can also be marked as {\tt closed binder} in
+which case only well-bracketed binders of the form {\tt (a b c:T)} or
+{\tt \{a b c:T\}} etc. are accepted.
+
+With closed binders, the recursive sequence in the left-hand side can
+be of the general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an
+arbitrary sequence of tokens. With open binders though, $s$ has to be
+empty. Here is an example of recursive notation with closed binders:
+
+\begin{coq_example*}
+Notation "'mylet' f x .. y :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (x closed binder, y closed binder, at level 200, right associativity).
+\end{coq_example*}
+
 \subsection{Summary}
 
 \paragraph{Syntax of notations}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 95a669f75..1c76aabbc 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -176,9 +176,10 @@ let rec check_same_type ty1 ty2 =
       check_same_type b1 b2
   | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
       check_same_type a1 a2
-  | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+  | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when n1=n2 ->
       List.iter2 check_same_type e1 e2;
-      List.iter2 (List.iter2 check_same_type) el1 el2
+      List.iter2 (List.iter2 check_same_type) el1 el2;
+      List.iter2 check_same_fix_binder bl1 bl2
   | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
       check_same_type e1 e2
@@ -285,7 +286,7 @@ and spaces ntn n =
   if n = String.length ntn then []
   else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
 
-let expand_curly_brackets loc mknot ntn (l,ll) =
+let expand_curly_brackets loc mknot ntn l =
   let ntn' = ref ntn in
   let rec expand_ntn i =
     function
@@ -298,12 +299,12 @@ let expand_curly_brackets loc mknot ntn (l,ll) =
             ntn' :=
               String.sub !ntn' 0 p ^ "_" ^
               String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",([a],[])) end
+            mknot (loc,"{ _ }",[a]) end
           else a in
         a' :: expand_ntn (i+1) l in
   let l = expand_ntn 0 l in
   (* side effect *)
-  mknot (loc,!ntn',(l,ll))
+  mknot (loc,!ntn',l)
 
 let destPrim = function CPrim(_,t) -> Some t | _ -> None
 let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -311,32 +312,34 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
   then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim (fst l),(snd l) with
+  else match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
-    | "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
-        mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
+    | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
+        mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
     | _ ->
 	match decompose_notation_key ntn, l with
-	| [Terminal "-"; Terminal x], ([],[]) ->
+	| [Terminal "-"; Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- 	     with _ -> mknot (loc,ntn,([],[])))
-	| [Terminal x], ([],[]) ->
+	     with _ -> mknot (loc,ntn,[]))
+	| [Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.of_string x))
- 	     with _ -> mknot (loc,ntn,([],[])))
+	     with _ -> mknot (loc,ntn,[]))
 	| _ ->
 	    mknot (loc,ntn,l)
 
-let make_notation loc ntn l =
+let make_notation loc ntn (terms,termlists,binders as subst) =
+  if termlists <> [] or binders <> [] then CNotation (loc,ntn,subst) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> CNotation (loc,ntn,l))
+    (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
     (fun (loc,p) -> CPrim (loc,p))
-    destPrim l
+    destPrim terms
 
-let make_pat_notation loc ntn l =
+let make_pat_notation loc ntn (terms,termlists as subst) =
+  if termlists <> [] then CPatNotation (loc,ntn,subst) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> CPatNotation (loc,ntn,l))
+    (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[])))
     (fun (loc,p) -> CPatPrim (loc,p))
-    destPatPrim l
+    destPatPrim terms
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
@@ -834,7 +837,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
-	let subst,substlist = match_aconstr t pat in
+	let terms,termlists,binders = match_aconstr t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
@@ -849,17 +852,21 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
 		        (scopt,scl@scopes') vars c)
-                      subst in
+                      terms in
 		  let ll =
 		    List.map (fun (c,(scopt,scl)) ->
 		      List.map (extern true (scopt,scl@scopes') vars) c)
-                      substlist in
-	          insert_delimiters (make_notation loc ntn (l,ll)) key)
+                      termlists in
+		  let bll =
+		    List.map (fun (bl,(scopt,scl)) ->
+		      snd (extern_local_binder (scopt,scl@scopes') vars bl))
+                      binders in
+	          insert_delimiters (make_notation loc ntn (l,ll,bll)) key)
           | SynDefRule kn ->
 	      let l =
 		List.map (fun (c,(scopt,scl)) ->
 		  extern true (scopt,scl@scopes) vars c, None)
-		  subst in
+		  terms in
               let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
 	      if l = [] then a else CApp (loc,(None,a),l) in
  	if args = [] then e
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 84327add6..25d13bc09 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -206,18 +206,18 @@ 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) =
+let contract_notation ntn (l,ll,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CNotation (_,"{ _ }",([a],[])) :: l ->
+    | 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)
+  !ntn',(l,ll,bll)
 
 let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
@@ -240,23 +240,65 @@ let make_current_scope = function
   | (Some tmp_scope,scopes) -> tmp_scope::scopes
   | None,scopes -> scopes
 
-let set_var_scope loc id (_,_,scopt,scopes) varscopes =
-  let idscopes = List.assoc id varscopes in
-  if !idscopes <> None &
-    make_current_scope (Option.get !idscopes)
-    <> make_current_scope (scopt,scopes) then
-      let pr_scope_stack = function
-	| [] -> str "the empty scope stack"
-	| [a] -> str "scope " ++ str a
-	| l -> str "scope stack " ++
-	    str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in
-      user_err_loc (loc,"set_var_scope",
-      pr_id id ++ str " is used both in " ++ 
-	pr_scope_stack (make_current_scope (Option.get !idscopes)) ++
-	strbrk " and in " ++
-	pr_scope_stack (make_current_scope (scopt,scopes)))
-  else
-    idscopes := Some (scopt,scopes)
+let pr_scope_stack = function
+  | [] -> str "the empty scope stack"
+  | [a] -> str "scope " ++ str a
+  | l -> str "scope stack " ++
+      str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
+
+let error_inconsistent_scope loc id scopes1 scopes2 =
+  user_err_loc (loc,"set_var_scope",
+    pr_id id ++ str " is used both in " ++
+    pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2)
+
+let error_expect_constr_notation_type loc id =
+  user_err_loc (loc,"",
+    pr_id id ++ str " is bound in the notation to a term variable.")
+
+let error_expect_binder_notation_type loc id =
+  user_err_loc (loc,"",
+    pr_id id ++
+    str " is expected to occur in binding position in the right-hand side.")
+
+let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
+  try
+    let idscopes,typ = List.assoc id ntnvars in
+    if !idscopes <> None &
+      make_current_scope (Option.get !idscopes)
+      <> make_current_scope (scopt,scopes) then
+	error_inconsistent_scope loc id
+	  (make_current_scope (Option.get !idscopes))
+	  (make_current_scope (scopt,scopes))
+    else
+      idscopes := Some (scopt,scopes);
+    match typ with
+    | NtnInternTypeBinder ->
+	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 -> ()
+  with Not_found ->
+    (* Not in a notation *)
+    ()
+
+let set_type_scope (ids,unb,tmp_scope,scopes) =
+  (ids,unb,Some Notation.type_scope,scopes)
+
+let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
+  (ids,unb,None,scopes)
+
+let rec it_mkRProd env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+    | [] -> body
+
+let rec it_mkRLambda env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+    | [] -> body
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
@@ -291,6 +333,7 @@ let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
       env
   | loc,Name id ->
       check_hidden_implicit_parameters id lvar;
+      set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars);
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
       (Idset.add id ids,unb,tmpsc,scopes)
@@ -325,7 +368,7 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
       | Default k ->
-          let (loc,na) = (List.hd nal) in
+          let (loc,na) = List.hd nal in
 	  (* TODO: fail if several names with different implicit types *)
 	  let ty = locate_if_isevar loc na (intern_type env ty) in
 	    List.fold_left
@@ -363,25 +406,53 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a
 	  (env', abs lid acc)) fvs (env,c)
   in c'
 
+let iterate_binder intern lvar (env,bl) = function
+  | LocalRawAssum(nal,bk,ty) ->
+      let intern_type env = intern (set_type_scope env) in
+      (match bk with
+      | Default k ->
+          let (loc,na) = List.hd nal in
+	  (* TODO: fail if several names with different implicit types *)
+	  let ty = intern_type env ty in
+	  let ty = locate_if_isevar loc na ty in
+	  List.fold_left
+	    (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+	    (env,bl) nal
+      | Generalized (b,b',t) ->
+	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
+	    env, b @ bl)
+  | LocalRawDef((loc,na as locna),def) ->
+      (push_name_env lvar env locna,
+      (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))=
+let option_mem_assoc id = function
+  | Some (id',c) -> id = id'
+  | None -> false
+
+let find_fresh_name renaming (terms,termlists,binders) id =
+  let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) terms in
+  let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) termlists) in
+  let fvs3 = List.map snd renaming in
+  (* TODO binders *)
+  let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
+  next_ident_away id fvs
+
+let traverse_binder (terms,_,_ as subst)
+    (renaming,(ids,unb,tmpsc,scopes as env))=
  function
  | Anonymous -> (renaming,env),Anonymous
  | Name id ->
   try
     (* Binders bound in the notation are considered first-order objects *)
-    let _,na = coerce_to_name (fst (List.assoc id subst)) in
+    let _,na = coerce_to_name (fst (List.assoc id terms)) in
     (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
-    let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
-    let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in
-    let fvs3 = List.map snd renaming in
-    let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
-    let id' = next_ident_away id fvs in
+    let id' = find_fresh_name renaming subst id in
     let renaming' = if id=id' then renaming else (id,id')::renaming in
     (renaming',env), Name id'
 
@@ -389,17 +460,18 @@ let rec subst_iterator y t = function
   | RVar (_,id) as x -> if id = y then t else x
   | x -> map_rawconstr (subst_iterator y t) x
 
-let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
-  let (renaming,(ids,unb,_,scopes)) = infos in
-  let subinfos = renaming,(ids,unb,None,scopes) in
-  match c with
-  | AVar id ->
+let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
+  let (terms,termlists,binders) = subst in
+  let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c =
+    let subinfos = renaming,(ids,unb,None,scopes) in
+    match c with
+    | AVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
 	try
-	  let (a,(scopt,subscopes)) = List.assoc id subst in
-	  interp (ids,unb,scopt,subscopes@scopes) a
+	  let (a,(scopt,subscopes)) = List.assoc id terms in
+	  intern (ids,unb,scopt,subscopes@scopes) a
 	with Not_found ->
 	try
 	  RVar (loc,List.assoc id renaming)
@@ -407,51 +479,64 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  RVar (loc,id)
       end
-  | AList (x,_,iter,terminator,lassoc) ->
+    | AList (x,_,iter,terminator,lassoc) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (l,(scopt,subscopes)) = List.assoc x substlist in
-        let termin =
-          subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
+	let (l,(scopt,subscopes)) = List.assoc x termlists in
+        let termin = aux subst' subinfos terminator in
 	List.fold_right (fun a t ->
           subst_iterator ldots_var t
-            (subst_aconstr_in_rawconstr loc interp
-              ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
+            (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter))
             (if lassoc then List.rev l else l) termin
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
-  | AHole (Evd.BinderType (Name id as na)) ->
+    | AHole (Evd.BinderType (Name id as na)) ->
       let na =
-        try snd (coerce_to_name (fst (List.assoc id subst)))
+        try snd (coerce_to_name (fst (List.assoc id terms)))
         with Not_found -> na in
       RHole (loc,Evd.BinderType na)
-  | t ->
-      rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
-      (subst_aconstr_in_rawconstr loc interp sub) subinfos t
-
-let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
-  let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
-  let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+    | ABinderList (x,_,iter,terminator) ->
+      (try
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (bl,(scopt,subscopes)) = List.assoc x binders in
+	let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in
+        let termin = aux subst' (renaming,env) terminator in
+	List.fold_left (fun t binder ->
+          subst_iterator ldots_var t
+	    (aux (terms,Some(x,binder)) subinfos iter))
+	  termin bl
+      with Not_found ->
+          anomaly "Inconsistent substitution of recursive notation")
+    | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
+	let (na,bk,_,t) = snd (Option.get binderopt) in
+	RProd (loc,na,bk,t,aux subst' infos c')
+    | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
+	let (na,bk,_,t) = snd (Option.get binderopt) in
+	RLambda (loc,na,bk,t,aux subst' infos c')
+    | t ->
+      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+	(aux subst') subinfos t
+  in aux (terms,None) infos c
+
+let split_by_type ids =
+  List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
+    match typ with
+    | NtnTypeConstr -> ((x,scl)::l1,l2,l3)
+    | NtnTypeConstrList -> (l1,(x,scl)::l2,l3)
+    | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[])
+
+let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l
+
+let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs =
+  let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
+  let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in
   Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
-  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-  let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
-  subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
-
-let set_type_scope (ids,unb,tmp_scope,scopes) =
-  (ids,unb,Some Notation.type_scope,scopes)
-
-let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
-  (ids,unb,None,scopes)
-
-let rec it_mkRProd env body =
-  match env with
-      (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
-    | [] -> body
-
-let rec it_mkRLambda env body =
-  match env with
-      (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
-    | [] -> body
+  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
+  subst_aconstr_in_rawconstr loc intern lvar
+    (terms,termlists,binders) ([],env) c
 
 (**********************************************************************)
 (* Discriminating between bound variables and global references       *)
@@ -479,7 +564,11 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
   (* Is [id] a notation variable *)
   else if List.mem_assoc id ntnvars
   then
-    (set_var_scope loc id genv ntnvars; RVar (loc,id), [], [], [])
+    (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], [])
+  (* Is [id] the special variable for recursive notations *)
+  else if ntnvars <> [] && id = ldots_var
+  then
+    RVar (loc,id), [], [], []
   else
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
   try
@@ -534,7 +623,7 @@ let intern_reference ref =
     (intern_extended_global_of_qualid (qualid_of_reference ref))
 
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid intern env args =
+let intern_qualid loc qid intern env lvar args =
   match intern_extended_global_of_qualid (loc,qid) with
   | TrueGlobal ref ->
       RRef (loc, ref), args
@@ -544,25 +633,25 @@ let intern_qualid loc qid intern env args =
       if List.length args < nids then error_not_enough_arguments loc;
       let args1,args2 = list_chop nids args in
       check_no_explicitation args1;
-      let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
-      subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
+      let subst = make_subst ids (List.map fst args1) in
+      subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env args =
-  match intern_qualid loc qid intern env args with
+let intern_non_secvar_qualid loc qid intern env lvar args =
+  match intern_qualid loc qid intern env lvar args with
     | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
 let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
   | Qualid (loc, qid) ->
-      let r,args2 = intern_qualid loc qid intern env args in
+      let r,args2 = intern_qualid loc qid intern env lvar args in
       find_appl_head_data r, args2
   | Ident (loc, id) ->
       try intern_var env lvar loc id, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
-	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
+	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
 	find_appl_head_data r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
@@ -904,7 +993,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
       intern_pat scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, fullargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
-      let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+      let (ids',idsl',_) = split_by_type ids' in
       Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
@@ -1090,12 +1180,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CLetIn (loc,na,c1,c2) ->
 	RLetIn (loc, snd na, intern (reset_tmp_scope env) c1,
           intern (push_name_env lvar env na) c2)
-    | CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
+    | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
-    | CNotation (_,"( _ )",([a],[])) -> intern env a
+    | CNotation (_,"( _ )",([a],[],[])) -> intern env a
     | CNotation (loc,ntn,args) ->
-        intern_notation intern env loc ntn args
+        intern_notation intern env lvar loc ntn args
     | CGeneralization (loc,b,a,c) ->
         intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
@@ -1118,8 +1208,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	let (c,impargs,args_scopes,l),args =
           match f with
             | CRef ref -> intern_applied_reference intern env lvar args ref
-            | CNotation (loc,ntn,([],[])) ->
-                let c = intern_notation intern env loc ntn ([],[]) in
+            | CNotation (loc,ntn,([],[],[])) ->
+                let c = intern_notation intern env lvar loc ntn ([],[],[]) in
                 find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
@@ -1260,8 +1350,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
       match bk with
 	| Default b -> default env b nal
 	| Generalized (b,b',t) ->
-	    let env, ibind = intern_generalized_binder intern_type lvar
-	      env [] (List.hd nal) b b' t ty in
+	    let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 
@@ -1276,8 +1365,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     in match bk with
       | Default b -> default env b nal
       | Generalized (b, b', t) ->
-	  let env, ibind = intern_generalized_binder intern_type lvar
-	    env [] (List.hd nal) b b' t ty in
+	  let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 
@@ -1440,19 +1528,20 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_rawconstr c
 
-let interp_aconstr ?(impls=[]) (vars,varslist) a =
+let interp_aconstr ?(impls=[]) vars recvars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
+  let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
   let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, [])
     false (([],[]),Environ.named_context env,vl,impls) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
-  let a = aconstr_of_rawconstr vars c in
+  let a = aconstr_of_rawconstr vars recvars c in
+  (* 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 = List.map (fun (id,(sc,typ)) -> (id,(out_scope !sc,typ))) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
-  (* Variables occurring in binders have no relevant scope since bound *)
-  let vl = List.map (fun (id,r) ->
-    (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
-  list_chop (List.length vars) vl, a
+  vars, a
 
 (* Interpret binders and contexts  *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index e1f1c50b4..642fc25af 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -171,10 +171,14 @@ val construct_reference : named_context -> identifier -> constr
 val global_reference : identifier -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
-(** Interprets into a abbreviatable constr *)
-
+(** Interprets a term as the left-hand side of a notation; the boolean
+    list is a set and this set is [true] for a variable occurring in
+    term position, [false] for a variable occurring in binding
+    position; [true;false] if in both kinds of position *)
 val interp_aconstr : ?impls:internalization_env ->
-  identifier list * identifier list -> constr_expr -> interpretation
+  (identifier * notation_var_internalization_type) list ->
+  (identifier * identifier) list -> constr_expr ->
+  (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cad48a5a1..7dbffe668 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -91,7 +91,7 @@ let is_freevar ids env x =
       with _ -> not (is_global x)
   with _ -> true
 
-(* Auxilliary functions for the inference of implicitly quantified variables. *)
+(* Auxiliary functions for the inference of implicitly quantified variables. *)
 
 let ungeneralizable loc id =
   user_err_loc (loc, "Generalization", 
@@ -108,7 +108,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (loc,id)) -> found loc id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) ->
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
diff --git a/interp/notation.ml b/interp/notation.ml
index 31e242c1f..a94da4331 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -207,7 +207,8 @@ let cases_pattern_key = function
 
 let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
   | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_,_)
+  | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args)
   | ARef ref -> RefKey(make_gr ref), None
   | _ -> Oth, None
 
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 16d0537b9..3eec1a3ab 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -51,6 +51,7 @@ let ppcmd_of_cut = function
 type unparsing =
   | UnpMetaVar of int * parenRelation
   | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 99152c045..d5f32dd2a 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -39,6 +39,7 @@ val ppcmd_of_cut : ppcut -> std_ppcmds
 type unparsing =
   | UnpMetaVar of int * parenRelation
   | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpBinderListMetaVar of int * bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 334135eaf..7790e56d5 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -74,8 +74,8 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr
 
 (* Coercions to the general format of notation that also supports
    variables bound to list of expressions *)
-let in_pat (ids,ac) = ((ids,[]),ac)
-let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
+let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
+let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
 
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index db6de8fd1..99dd32868 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -34,6 +34,7 @@ type aconstr =
   (* Part only in rawconstr *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
+  | ABinderList of identifier * identifier * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
@@ -48,6 +49,21 @@ type aconstr =
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
 
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+type notation_var_instance_type =
+  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+
+type notation_var_internalization_type =
+  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+
+type interpretation =
+    (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+
 (**********************************************************************)
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
 
@@ -67,6 +83,16 @@ let rec cases_pattern_fold_map loc g e = function
 
 let rec subst_rawvars l = function
   | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
+  | RProd (loc,Name id,bk,t,c) ->
+      let id =
+	try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+	with Not_found -> id in
+      RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
+  | RLambda (loc,Name id,bk,t,c) ->
+      let id =
+	try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+	with Not_found -> id in
+      RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
   | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *)
 
 let ldots_var = id_of_string ".."
@@ -80,6 +106,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
+  | ABinderList (x,y,iter,tail) ->
+      let t = f e tail in let it = f e iter in
+      let innerl = [(ldots_var,t);(x,RVar(loc,y))] in
+      let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
+      let outerl = [(ldots_var,inner)] in
+      subst_rawvars outerl it
   | ALambda (na,ty,c) ->
       let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
   | AProd (na,ty,c) ->
@@ -132,72 +164,135 @@ let rec rawconstr_of_aconstr loc x =
 (****************************************************************************)
 (* Translating a rawconstr into a notation, interpreting recursive patterns *)
 
-let add_name r = function
-  | Anonymous -> ()
-  | Name id -> r := id :: !r
+let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
+let add_name r = function Anonymous -> () | Name id -> add_id r id
 
-let has_ldots =
-  List.exists
-    (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
-
-let compare_rawconstr f t1 t2 = match t1,t2 with
-  | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 
-  | RVar (_,v1), RVar (_,v2) -> v1 = v2
-  | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
-  | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
-      f ty1 ty2 & f c1 c2
+let split_at_recursive_part c =
+  let sub = ref None in
+  let rec aux = function
+  | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var ->
+      if !sub <> None then
+	(* Not narrowed enough to find only one recursive part *)
+	raise Not_found
+      else
+	(sub := Some c;
+	 if l = [] then RVar (loc,ldots_var)
+	 else RApp (loc0,RVar (loc,ldots_var),l))
+  | c -> map_rawconstr aux c in
+  let outer_iterator = aux c in
+  match !sub with
+  | None -> (* No recursive pattern found *) raise Not_found
+  | Some c ->
+  match outer_iterator with
+  | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found
+  | _ -> outer_iterator, c
+
+let on_true_do b f c = if b then (f c; b) else b
+
+let compare_rawconstr f add t1 t2 = match t1,t2 with
+  | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2
+  | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
+  | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
+  | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
   | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
-      f ty1 ty2 & f c1 c2
+      on_true_do (f ty1 ty2 & f c1 c2) add na1
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
-  | (RLetIn _ | RCases _ | RRec _ | RDynamic _
+  | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 ->
+      on_true_do (f b1 b2 & f c1 c2) add na1
+  | (RCases _ | RRec _ | RDynamic _
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
-  | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
+  | _,(RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations."
-  | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
+  | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _
+    | RHole _ | RSort _ | RLetIn _), _
       -> false
 
-let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
+let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2
+
+let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1)
 
-let discriminate_patterns foundvars nl l1 l2 =
+let check_is_hole id = function RHole _ -> () | t ->
+  user_err_loc (loc_of_rawconstr t,"",
+    strbrk "In recursive notation with binders, " ++ pr_id id ++
+    strbrk " is expected to come without type.")
+
+let compare_recursive_parts found f (iterator,subc) =
   let diff = ref None in
-  let rec aux n c1 c2 = match c1,c2 with
-  | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
-      if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
-      else
-        !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
-        or (error
-          "Both ends of the recursive pattern differ in more than one place")
-  | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
-  let l = list_map2_i aux 0 l1 l2 in
-  if not (List.for_all ((=) true) l) then
-    error "Both ends of the recursive pattern differ.";
-  match !diff with
-    | None ->  error "Both ends of the recursive pattern are the same."
-    | Some (x,y,_ as discr) ->
-	List.iter (fun id ->
-          if List.mem id !foundvars
-          then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part.");
-          foundvars := id::!foundvars) [x;y];
-	discr
+  let terminator = ref None in
+  let rec aux c1 c2 = match c1,c2 with
+  | RVar(_,v), term when v = ldots_var ->
+      (* We found the pattern *)
+      assert (!terminator = None); terminator := Some term;
+      true
+  | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var ->
+      (* We found the pattern, but there are extra arguments *)
+      (* (this allows e.g. alternative (recursive) notation of application) *)
+      assert (!terminator = None); terminator := Some term;
+      list_for_all2eq aux l1 l2
+  | RVar (_,x), RVar (_,y) when x<>y ->
+      (* We found the position where it differs *)
+      let lassoc = (!terminator <> None) in
+      let x,y = if lassoc then y,x else x,y in
+      !diff = None && (diff := Some (x,y,Some lassoc); true)
+  | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term)
+  | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) ->
+      (* We found a binding position where it differs *)
+      check_is_hole y t_x;
+      check_is_hole y t_y;
+      !diff = None && (diff := Some (x,y,None); aux c term)
+  | _ ->
+      compare_rawconstr aux (add_name found) c1 c2 in
+  if aux iterator subc then
+    match !diff with
+    | None ->
+	let loc1 = loc_of_rawconstr iterator in
+	let loc2 = loc_of_rawconstr (Option.get !terminator) in
+	(* 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,Some lassoc) ->
+	let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+	let iterator =
+	  f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator
+	  else iterator) in
+	(* found have been collected by compare_constr *)
+	found := newfound;
+	AList (x,y,iterator,f (Option.get !terminator),lassoc)
+    | Some (x,y,None) ->
+	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
+	let iterator = f iterator in
+	(* found have been collected by compare_constr *)
+	found := newfound;
+	ABinderList (x,y,iterator,f (Option.get !terminator))
+  else
+    raise Not_found
 
 let aconstr_and_vars_of_rawconstr a =
-  let found = ref [] in
-  let rec aux = function
-  | RVar (_,id) -> found := id::!found; AVar id
-  | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
-  | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
-      (* Special case for alternative (recursive) notation of application *)
-      let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
-      found := ldots_var :: !found; assert lassoc;
-      AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
+  let found = ref ([],[],[]) in
+  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' (split_at_recursive_part c)
+    with Not_found ->
+    found := keepfound;
+    match c with
+    | RApp (_,RVar (loc,f),[c]) when f = ldots_var ->
+	(* Fall on the second part of the recursive pattern w/o having
+	   found the first part *)
+	user_err_loc (loc,"",
+	str "Cannot find where the recursive pattern starts.")
+    | c ->
+	aux' c
+  and aux' = function
+  | RVar (_,id) -> add_id found id; AVar id
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
   | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
   | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
   | RCases (_,sty,rtntypopt,tml,eqnl) ->
-      let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
+      let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
       ACases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
@@ -213,7 +308,7 @@ let aconstr_and_vars_of_rawconstr a =
       add_name found na;
       AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
   | RRec (_,fk,idl,dll,tl,bl) ->
-      Array.iter (fun id -> found := id::!found) idl;
+      Array.iter (add_id found) idl;
       let dll = Array.map (List.map (fun (na,bk,oc,b) ->
 	 if bk <> Explicit then
 	   error "Binders marked as implicit not allowed in notations.";
@@ -229,51 +324,61 @@ let aconstr_and_vars_of_rawconstr a =
   | RDynamic _ | REvar _ ->
       error "Existential variables not allowed in notations."
 
-  (* Recognizing recursive notations *)
-  and terminator_of_pat f1 ll1 lr1 = function
-  | RApp (loc,f2,l2) ->
-      if not (eq_rawconstr f1 f2) then errorlabstrm ""
-	(strbrk "Cannot recognize the same head to both ends of the recursive pattern.");
-      let nl = List.length ll1 in
-      let nr = List.length lr1 in
-      if List.length l2 <> nl + nr + 1 then
-	error "Both ends of the recursive pattern have different lengths.";
-      let ll2,l2' = list_chop nl l2 in
-      let t = List.hd l2' and lr2 = List.tl l2' in
-      let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
-      let iter =
-        if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
-        else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
-      (if order then y else x),(if order then x else y), aux iter, aux t, order
-  | _ -> error "One end of the recursive pattern is not an application."
-
-  and make_aconstr_list f args =
-    let rec find_patterns acc = function
-      | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
-          (* We've found the recursive part *)
-	  let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
-	  AList (x,y,iter,term,lassoc)
-      | a::l -> find_patterns (a::acc) l
-      | [] -> error "Ill-formed recursive notation."
-    in find_patterns [] args
-
   in
   let t = aux a in
   (* Side effect *)
   t, !found
 
-let aconstr_of_rawconstr vars a =
-  let a,foundvars = aconstr_and_vars_of_rawconstr a in
-  let check_type x =
-    if not (List.mem x foundvars) then
-      error ((string_of_id x)^" is unbound in the right-hand-side.") in
-  List.iter check_type vars;
+let rec list_rev_mem_assoc x = function
+  | [] -> false
+  | (_,x')::l -> x = x' || list_rev_mem_assoc x l
+
+let check_variables vars recvars (found,foundrec,foundrecbinding) =
+  let useless_vars = List.map snd recvars in
+  let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in
+  let check_recvar x =
+    if List.mem x found then
+      errorlabstrm "" (pr_id x ++
+	strbrk " should only be used in the recursive part of a pattern.") in
+  List.iter (fun (x,y) -> check_recvar x; check_recvar y)
+    (foundrec@foundrecbinding);
+  let check_bound x =
+    if not (List.mem x found) then
+      if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding
+	or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding
+      then
+	error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.")
+      else
+	error ((string_of_id x)^" is unbound in the right-hand side.") in
+  let check_pair s x y where =
+    if not (List.mem (x,y) where) then
+      errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+	str " and " ++ pr_id 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 ->
+	begin
+	  try check_pair "term" x (List.assoc x recvars) foundrec
+	  with Not_found -> check_bound x
+	end
+    | NtnInternTypeBinder ->
+	begin
+	  try check_pair "binding" x (List.assoc x recvars) foundrecbinding
+	  with Not_found -> check_bound x
+	end
+    | NtnInternTypeIdent -> check_bound x in
+  List.iter check_type vars
+
+let aconstr_of_rawconstr vars recvars a =
+  let a,found = aconstr_and_vars_of_rawconstr a in
+  check_variables vars recvars found;
   a
 
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let aconstr_of_constr avoiding t =
- aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
+ aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t)
 
 let rec subst_pat subst pat =
   match pat with
@@ -317,6 +422,12 @@ let rec subst_aconstr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  AProd (n,r1',r2')
 
+  | ABinderList (id1,id2,r1,r2) ->
+      let r1' = subst_aconstr subst bound r1
+      and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ABinderList (id1,id2,r1',r2')
+
   | ALetIn (n,r1,r2) ->
       let r1' = subst_aconstr subst bound r1
       and r2' = subst_aconstr subst bound r2 in
@@ -394,7 +505,7 @@ let rec subst_aconstr subst bound raw =
 		ACast (r1',CastCoerce)
 
 let subst_interpretation subst (metas,pat) =
-  let bound = List.map fst (fst metas @ snd metas) in
+  let bound = List.map fst metas in
   (metas,subst_aconstr subst bound pat)
 
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
@@ -432,7 +543,7 @@ let rec alpha_var id1 id2 = function
 
 let alpha_eq_val (x,y) = x = y
 
-let bind_env alp (sigma,sigmalist as fullsigma) var v =
+let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
   try
     let vvar = List.assoc var sigma in
     if alpha_eq_val (v,vvar) then fullsigma
@@ -441,7 +552,10 @@ let bind_env alp (sigma,sigmalist as fullsigma) var v =
     (* Check that no capture of binding variables occur *)
     if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
     (* TODO: handle the case of multiple occs in different scopes *)
-    ((var,v)::sigma,sigmalist)
+    ((var,v)::sigma,sigmalist,sigmabinders)
+
+let bind_binder (sigma,sigmalist,sigmabinders) x bl =
+  (sigma,sigmalist,(x,List.rev bl)::sigmabinders)
 
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
@@ -456,13 +570,9 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | Some t1, Some t2 -> f sigma t1 t2
   | _ -> raise No_match
 
-let rawconstr_of_name = function
-  | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
-  | Name id -> RVar (dummy_loc,id)
-
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (na,Name id2) when List.mem id2 metas ->
-      alp, bind_env alp sigma id2 (rawconstr_of_name na)
+  | (Name id1,Name id2) when List.mem id2 metas ->
+      alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
@@ -480,33 +590,80 @@ let adjust_application_n n loc f l =
   let l1,l2 = list_chop (List.length l - n) l in
   if l1 = [] then f,l else RApp (loc,f,l1), l2
 
-let match_alist match_fun metas sigma l1 l2 x iter termin lassoc =
-  (* match the iterator at least once *)
-  let sigmavar,sigmalist =
-    List.fold_left2 (match_fun (ldots_var::metas)) sigma l1 l2 in
-  (* Recover the recursive position *)
-  let rest = List.assoc ldots_var sigmavar in
-  (* Recover the first element *)
-  let t1 = List.assoc x sigmavar in
-  let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
-  (* try to find the remaining elements or the terminator *)
-  let rec match_alist_tail metas sigma acc rest =
+let glue_letin_with_decls = true
+
+let rec match_iterated_binders islambda decls = function
+  | RLambda (_,na,bk,t,b) when islambda ->
+      match_iterated_binders islambda ((na,bk,None,t)::decls) b
+  | RProd (_,(Name _ as na),bk,t,b) when not islambda ->
+      match_iterated_binders islambda ((na,bk,None,t)::decls) b
+  | RLetIn (loc,na,c,b) when glue_letin_with_decls ->
+      match_iterated_binders islambda
+	((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b
+  | b -> (decls,b)
+
+let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
+  (List.remove_assoc x sigmavar,sigmalist,sigmabinders)
+
+let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
+  let rec aux sigma acc rest =
     try
-      let sigmavar,sigmalist = match_fun (ldots_var::metas) sigma rest iter in
-      let rest = List.assoc ldots_var sigmavar in
-      let t = List.assoc x sigmavar in
-      let sigmavar =
-	List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
-      match_alist_tail metas (sigmavar,sigmalist) (t::acc) rest
-    with No_match ->
-      List.rev acc, match_fun metas (sigmavar,sigmalist) rest termin in
-  let tl,(sigmavar,sigmalist) = match_alist_tail metas sigma [t1] rest in
-  (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
+      let sigma = match_fun (ldots_var::metas) sigma rest iter in
+      let rest = List.assoc ldots_var (pi1 sigma) in
+      let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in
+      let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+      aux sigma (b::acc) rest
+    with No_match when acc <> [] ->
+      acc, match_fun metas sigma rest termin in
+  let bl,sigma = aux sigma [] rest in
+  bind_binder sigma x bl
+
+let match_alist match_fun metas sigma rest x iter termin lassoc =
+  let rec aux sigma acc rest =
+    try
+      let sigma = match_fun (ldots_var::metas) sigma rest iter in
+      let rest = List.assoc ldots_var (pi1 sigma) in
+      let t = List.assoc x (pi1 sigma) in
+      let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+      aux sigma (t::acc) rest
+    with No_match when acc <> [] ->
+      acc, match_fun metas sigma rest termin in
+  let l,sigma = aux sigma [] rest in
+  (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
 
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
+
+  (* Matching notation variable *)
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
+
+  (* Matching recursive notations for terms *)
+  | r1, AList (x,_,iter,termin,lassoc) ->
+      match_alist (match_ alp) metas sigma r1 x iter termin lassoc
+
+  (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
+  | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)->
+      let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
+      (* TODO: address the possibility that termin is a Lambda itself *)
+      match_ alp metas (bind_binder sigma x decls) b termin
+  | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin)
+      when na1 <> Anonymous ->
+      let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
+      (* TODO: address the possibility that termin is a Prod itself *)
+      match_ alp metas (bind_binder sigma x decls) b termin
+  (* Matching recursive notations for binders: general case *)
+  | r, ABinderList (x,_,iter,termin) ->
+      match_abinderlist_with_app (match_ alp) metas sigma r x iter termin
+
+  (* Matching individual binders *)
+  | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id metas ->
+      match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+  | RProd (_,na,bk,t,b1), AProd (Name id,_,b2)
+      when List.mem id metas & na <> Anonymous ->
+      match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+
+  (* Matching compositionally *)
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
-  | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma 
+  | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
   | RApp (loc,f1,l1), AApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
@@ -517,11 +674,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
 	  let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
-  | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
-      when List.length l1 >= List.length l2 ->
-      let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
-      match_alist (match_ alp)
-	metas sigma (f1::l1) (f2::l2) x iter termin lassoc
   | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
@@ -586,38 +738,35 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_ alp metas sigma rhs1 rhs2
 
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-type interpretation =
-    (* regular vars of notation    / recursive parts of notation    / body *)
-    ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
-
-let match_aconstr c ((metas_scl,metaslist_scl),pat) =
-  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
-  let subst,substlist = match_ [] vars ([],[]) c pat in
+let match_aconstr c (metas,pat) =
+  let vars = List.map fst metas in
+  let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find x =
-    try List.assoc x subst
+    try List.assoc x terms
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
       RVar (dummy_loc,x) in
-  List.map (fun (x,scl) -> (find x,scl)) metas_scl,
-  List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
+  List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
+    match typ with
+    | NtnTypeConstr ->
+       ((find x, scl)::terms',termlists',binders')
+    | NtnTypeConstrList ->
+       (terms',(List.assoc x termlists,scl)::termlists',binders')
+    | NtnTypeBinderList ->
+       (terms',termlists',(List.assoc x binders,scl)::binders'))
+    metas ([],[],[])
 
 (* Matching cases pattern *)
 
-let bind_env_cases_pattern (sigma,sigmalist as fullsigma) var v =
+let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
     let vvar = List.assoc var sigma in
     if v=vvar then fullsigma else raise No_match
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma,sigmalist
+    (var,v)::sigma,sigmalist,x
 
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1
@@ -637,26 +786,33 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
         (* All parameters must be _ *)
         List.iter (function AHole _ -> () | _ -> raise No_match) p2;
 	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+  | r1, AList (x,_,iter,termin,lassoc) ->
+      match_alist match_cases_pattern
+	metas (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc
+(*
   | PatCstr (loc,(ind,_ as r1),args1,_),
-    AList (x,_,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
+    AList (x,y,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
       when r1 = r2 ->
       let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
       assert (List.length args1 + nparams = List.length l2);
       let (p2,args2) = list_chop nparams l2 in
       List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+      let x = if lassoc then x else y in
       match_alist match_cases_pattern
-	metas sigma args1 args2 x iter termin lassoc
+	metas (pi1 sigma,pi2 sigma,()) args1 args2 x iter termin lassoc
+*)
   | _ -> raise No_match
 
-let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
-  let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
-  let subst,substlist = match_cases_pattern vars ([],[]) c pat in
+let match_aconstr_cases_pattern c (metas,pat) =
+  let vars = List.map fst metas in
+  let terms,termlists,() = match_cases_pattern vars ([],[],()) c pat in
   (* Reorder canonically the substitution *)
-  let find x subst =
-    try List.assoc x subst
-    with Not_found -> anomaly "match_aconstr_cases_pattern" in
-  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
-  List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
+  List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
+    match typ with
+    | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists')
+    | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists')
+    | NtnTypeBinderList -> assert false)
+    metas ([],[])
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
@@ -673,19 +829,20 @@ type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
 
-type 'a notation_substitution =
-    'a list * (* for recursive notations: *) 'a list list
-
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
+  | CPatNotation of loc * notation * cases_pattern_notation_substitution
   | CPatPrim of loc * prim_token
-  | CPatRecord of loc * (reference * cases_pattern_expr) list
+  | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
+and cases_pattern_notation_substitution =
+    cases_pattern_expr list *     (** for constr subterms *)
+    cases_pattern_expr list list  (** for recursive notations *)
+
 type constr_expr =
   | CRef of reference
   | CFix of loc * identifier located * fix_expr list
@@ -710,7 +867,7 @@ type constr_expr =
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_expr notation_substitution
+  | CNotation of loc * notation * constr_notation_substitution
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -719,14 +876,6 @@ type constr_expr =
 and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
-and local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * binder_kind * constr_expr
-
-and typeclass_constraint = name located * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
 and cofix_expr =
     identifier located * local_binder list * constr_expr * constr_expr
 
@@ -735,6 +884,19 @@ and recursion_order_expr =
   | CWfRec of constr_expr
   | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
 
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * binder_kind * constr_expr
+
+and constr_notation_substitution =
+    constr_expr list *      (* for constr subterms *)
+    constr_expr list list * (* for recursive notations *)
+    local_binder list list      (* for binders subexpressions *)
+
+type typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
+
 type constr_pattern_expr = constr_expr
 
 (***********************)
@@ -787,6 +949,15 @@ let cases_pattern_expr_loc = function
   | CPatPrim (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
+let local_binder_loc = function
+  | LocalRawAssum ((loc,_)::_,_,t)
+  | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
+  | LocalRawAssum ([],_,_) -> assert false
+
+let local_binders_loc bll =
+  if bll = [] then dummy_loc else
+  join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+
 let occur_var_constr_ref id = function
   | Ident (loc,id') -> id = id'
   | Qualid _ -> false
@@ -796,7 +967,7 @@ let ids_of_cases_indtype =
   let rec vars_of = function
     (* We deal only with the regular cases *)
     | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
-    | CNotation (_,_,(l,[]))
+    | CNotation (_,_,(l,[],[]))
     (* assume the ntn is applicative and does not instantiate the head !! *)
     | CAppExpl (_,_,l) -> List.fold_left add_var [] l
     | CDelimiters(_,_,c) -> vars_of c
@@ -847,7 +1018,7 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | LocalRawDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | _ ->
+  | [] ->
       f n acc b
 
 let fold_constr_expr_with_binders g f n acc = function
@@ -858,7 +1029,11 @@ let fold_constr_expr_with_binders g f n acc = function
   | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
   | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
-  | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
+  | CNotation (_,_,(l,ll,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
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll
   | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
@@ -964,15 +1139,15 @@ let split_at_annot bl na =
   let names = List.map snd (names_of_local_assums bl) in
   match na with
   | None ->
-      if names = [] then error "A fixpoint needs at least one parameter." 
+      if names = [] then error "A fixpoint needs at least one parameter."
       else [], bl
   | Some (loc, id) ->
       let rec aux acc = function
 	| LocalRawAssum (bls, k, t) as x :: rest ->
 	    let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
-	      if r = [] then aux (x :: acc) rest 
-	      else 
-		(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), 
+	      if r = [] then aux (x :: acc) rest
+	      else
+		(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
 		 LocalRawAssum (r, k, t) :: rest)
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
 	| [] ->
@@ -1012,8 +1187,10 @@ let map_constr_expr_with_binders g f e = function
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
   | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
   | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
-  | CNotation (loc,n,(l,ll)) ->
-      CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
+  | CNotation (loc,n,(l,ll,bll)) ->
+      (* This is an approximation because we don't know what binds what *)
+      CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll,
+                     List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
   | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _
@@ -1074,16 +1251,21 @@ type 'a module_signature =
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
 
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
-(* and which are them occupied by proper symbols of the notation (or spaces) *)
+(* and which are then occupied by proper symbols of the notation (or spaces) *)
 
-let locs_of_notation f loc (args,argslist) ntn =
+let locs_of_notation loc locs ntn =
   let (bl,el) = Util.unloc loc in
+  let locs =  List.map Util.unloc locs in
   let rec aux pos = function
     | [] -> if pos = el then [] else [(pos,el-1)]
-    | a::l ->
-	let ba,ea = Util.unloc (f a) in
-	if pos = ba then aux ea l else (pos,ba-1)::aux ea l
-  in aux bl (args@List.flatten argslist)
+    | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+  in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs)
+
+let ntn_loc loc (args,argslist,binderslist) =
+  locs_of_notation loc
+    (List.map constr_loc (args@List.flatten argslist)@
+     List.map local_binders_loc binderslist)
 
-let ntn_loc = locs_of_notation constr_loc
-let patntn_loc = locs_of_notation cases_pattern_expr_loc
+let patntn_loc loc (args,argslist) =
+  locs_of_notation loc
+    (List.map cases_pattern_expr_loc (args@List.flatten argslist))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5ce488b9a..b5438dd7c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -31,6 +31,7 @@ type aconstr =
   (** Part only in [rawconstr] *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
+  | ABinderList of identifier * identifier * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
@@ -45,10 +46,33 @@ type aconstr =
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
 
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an aconstr: in a recursive pattern x..y,
+    x carries the sequence of objects bound to the list x..y  *)
+type notation_var_instance_type =
+  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as an aconstr:
+    in a recursive pattern x..y, both x and y carry the individual type
+    of each element of the list x..y *)
+type notation_var_internalization_type =
+  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+    (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+
 (** Translate a rawconstr into a notation given the list of variables
     bound by the notation; also interpret recursive patterns           *)
 
-val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+val aconstr_of_rawconstr :
+  (identifier * notation_var_internalization_type) list ->
+  (identifier * identifier) list -> rawconstr -> aconstr
 
 (** Name of the special identifier used to encode recursive notations  *)
 val ldots_var : identifier
@@ -64,23 +88,14 @@ val rawconstr_of_aconstr_with_binders : loc ->
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
-(** [match_aconstr metas] matches a rawconstr against an aconstr with
-   metavariables in [metas]; raise [No_match] if the matching fails   *)
+(** [match_aconstr] matches a rawconstr against a notation interpretation;
+    raise [No_match] if the matching fails   *)
 
 exception No_match
 
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-type interpretation =
-    (** regular vars of notation    / recursive parts of notation    / body *)
-    ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
-
 val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * subscopes) list * (rawconstr list * subscopes) list
+      (rawconstr * subscopes) list * (rawconstr list * subscopes) list *
+      (rawdecl list * subscopes) list
 
 val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
       (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list
@@ -107,19 +122,20 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
 
-type 'a notation_substitution =
-    'a list * (** for recursive notations: *) 'a list list
-
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
+  | CPatNotation of loc * notation * cases_pattern_notation_substitution
   | CPatPrim of loc * prim_token
   | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
+and cases_pattern_notation_substitution =
+    cases_pattern_expr list *     (** for constr subterms *)
+    cases_pattern_expr list list  (** for recursive notations *)
+
 type constr_expr =
   | CRef of reference
   | CFix of loc * identifier located * fix_expr list
@@ -144,7 +160,7 @@ type constr_expr =
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_expr notation_substitution
+  | CNotation of loc * notation * constr_notation_substitution
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -166,6 +182,11 @@ and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * binder_kind * constr_expr
 
+and constr_notation_substitution =
+    constr_expr list *      (** for constr subterms *)
+    constr_expr list list * (** for recursive notations *)
+    local_binder list list (** for binders subexpressions *)
+
 type typeclass_constraint = name located * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
@@ -178,6 +199,8 @@ val constr_loc : constr_expr -> loc
 
 val cases_pattern_expr_loc : cases_pattern_expr -> loc
 
+val local_binders_loc : local_binder list -> loc
+
 val replace_vars_constr_expr :
   (identifier * identifier) list -> constr_expr -> constr_expr
 
@@ -248,7 +271,6 @@ type 'a module_signature =
   | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
 
 val ntn_loc :
-  Util.loc -> constr_expr notation_substitution -> string -> (int * int) list
+  Util.loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
-  Util.loc -> cases_pattern_expr notation_substitution -> string ->
-  (int * int) list
+  Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index a32bfdec4..db28c866f 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -62,44 +62,53 @@ type grammar_constr_prod_item =
     (* tells action rule to make a list of the n previous parsed items; 
        concat with last parsed list if true *)
 
-type 'a action_env = 'a list * 'a list list
-
 let make_constr_action
-  (f : loc -> constr_expr action_env -> constr_expr) pil =
-  let rec make (env,envlist as fullenv : constr_expr action_env) = function
+  (f : loc -> constr_notation_substitution -> constr_expr) pil =
+  let rec make (constrs,constrlists,binders as fullsubst) = function
   | [] ->
-      Gram.action (fun loc -> f loc fullenv)
+      Gram.action (fun loc -> f loc fullsubst)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullenv tl)
+      Gram.action (fun _ -> make fullsubst tl)
   | GramConstrNonTerminal (typ, Some _) :: tl ->
       (* parse a binding non-terminal *)
     (match typ with
     | (ETConstr _| ETOther _) ->
-        Gram.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
+	Gram.action (fun (v:constr_expr) ->
+	  make (v :: constrs, constrlists, binders) tl)
     | ETReference ->
-        Gram.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
+        Gram.action (fun (v:reference) ->
+	  make (CRef v :: constrs, constrlists, binders) tl)
     | ETName ->
         Gram.action (fun (na:name located) ->
-	  make (constr_expr_of_name na :: env, envlist) tl)
+	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
     | ETConstrList (_,n) ->
-	Gram.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+	Gram.action (fun (v:constr_expr list) ->
+	  make (constrs, v::constrlists, binders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gram.action (fun (v:local_binder list) ->
+	  make (constrs, constrlists, v::binders) tl)
+    | ETBinderList (false,_) ->
+	Gram.action (fun (v:local_binder list list) ->
+	  make (constrs, constrlists, List.flatten v::binders) tl)
     | ETPattern ->
 	failwith "Unexpected entry of type cases pattern")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
-      let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      let heads,constrs = list_chop n constrs in
+      let constrlists =
+	if b then (heads@List.hd constrlists)::List.tl constrlists
+	else heads::constrlists
+      in make (constrs, constrlists, binders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],[]) (List.rev pil)
 
 let make_cases_pattern_action
-  (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
+  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
+  let rec make (env,envlist as fullenv) = function
   | [] ->
       Gram.action (fun loc -> f loc fullenv)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
@@ -122,7 +131,7 @@ let make_cases_pattern_action
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
 	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETOther _) ->
+    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
 	failwith "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
@@ -273,7 +282,10 @@ type notation_grammar =
     int * gram_assoc option * notation * grammar_constr_prod_item list list
 
 type all_grammar_command =
-  | Notation of (precedence * tolerability list) * notation_grammar
+  | Notation of
+	 (precedence * tolerability list) *
+	  notation_var_internalization_type list *
+	  notation_grammar
   | TacticGrammar of
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
@@ -282,14 +294,16 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 let extend_grammar gram =
   (match gram with
-  | Notation (_,a) -> extend_constr_notation a
+  | Notation (_,_,a) -> extend_constr_notation a
   | TacticGrammar g -> add_tactic_entry g);
   grammar_state := gram :: !grammar_state
 
 let recover_notation_grammar ntn prec =
   let l = map_succeed (function
-    | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x
-    | _ -> failwith "") !grammar_state in
+    | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+	 vars, x
+    | _ ->
+	 failwith "") !grammar_state in
   assert (List.length l = 1);
   List.hd l
 
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 56e6b1d61..05b2ddd99 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -45,7 +45,12 @@ type grammar_prod_item =
 (** Adding notations *)
 
 type all_grammar_command =
-  | Notation of (precedence * tolerability list) * notation_grammar
+  | Notation of
+	 (precedence * tolerability list)
+	  * notation_var_internalization_type list
+	   (** not needed for defining grammar, hosted by egrammar for
+	       transmission to interp_aconstr (via recover_notation_grammar) *)
+	  * notation_grammar
   | TacticGrammar of
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
@@ -61,5 +66,8 @@ val extend_vernac_command_grammar :
 val get_extend_vernac_grammars :
  unit -> (string * grammar_prod_item list list) list
 
+(** For a declared grammar, returns the rule + the ordered entry types
+    of variables in the rule (for use in the interpretation) *)
 val recover_notation_grammar :
-  notation -> (precedence * tolerability list) -> notation_grammar
+  notation -> (precedence * tolerability list) ->
+  notation_var_internalization_type list * notation_grammar
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 4674a7c90..f7daafb03 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -23,17 +23,19 @@ type production_level =
 
 type ('lev,'pos) constr_entry_key_gen =
   | ETName | ETReference | ETBigint
+  | ETBinder of bool (* true=open, as in "fun .."; false as in "let f .. :=" *)
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
 
 (**  Entries level (left-hand-side of grammar rules) *)
 
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
 
-(** Entries used in productions (in right-hand-side of grammar rules) *)
+(** Entries used in productions (in right-hand side of grammar rules) *)
 
 type constr_prod_entry_key =
     (production_level,production_position) constr_entry_key_gen
diff --git a/parsing/extend.mli b/parsing/extend.mli
index a05952294..fa2fef6b5 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -22,10 +22,12 @@ type production_level =
 
 type ('lev,'pos) constr_entry_key_gen =
   | ETName | ETReference | ETBigint
+  | ETBinder of bool
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
 
 (** Entries level (left-hand-side of grammar rules) *)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e3c898284..f74d28f0b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,11 +31,6 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
-let loc_of_binder = function
-  | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
-  | LocalRawDef ((loc,_),_)::_ -> loc
-  | _ -> dummy_loc
-
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
     LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
@@ -129,7 +124,7 @@ let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  closed_binder binders binders_fixannot
+  closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
@@ -202,7 +197,7 @@ GEXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CNotation(loc,"( _ )",([c],[]))
+                CNotation(loc,"( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -238,7 +233,7 @@ GEXTEND Gram
           mkCLambdaN loc bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = loc_of_binder bl in
+          let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
@@ -392,12 +387,15 @@ GEXTEND Gram
     (* Same as binders but parentheses around a closed binder are optional if
        the latter is unique *)
     [ [ (* open binder *)
-        idl = LIST1 name; ":"; c = lconstr ->
-          [LocalRawAssum (idl,Default Explicit,c)]
+        id = name; idl = LIST0 name; ":"; c = lconstr ->
+          [LocalRawAssum (id::idl,Default Explicit,c)]
 	(* binders factorized with open binder *)
-      | idl = LIST1 name; bl = binders ->
-          let t = CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))) in
-          LocalRawAssum (idl,Default Explicit,t)::bl
+      | id = name; idl = LIST0 name; bl = binders ->
+          let t = CHole (loc, Some (Evd.BinderType (snd id))) in
+          LocalRawAssum (id::idl,Default Explicit,t)::bl
+      | id1 = name; ".."; id2 = name ->
+          [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
+	                  Default Explicit,CHole (loc,None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
     ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3e5a52e46..e4513e58d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -931,6 +931,8 @@ GEXTEND Gram
   syntax_extension_type:
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
+      | IDENT "binder" -> ETBinder true
+      | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
   opt_scope:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 3cdf89ebd..1c35a2149 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -355,7 +355,9 @@ module Constr =
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let closed_binder = Gram.entry_create "constr:closed_binder"
+    let binder = Gram.entry_create "constr:binder"
     let binders = Gram.entry_create "constr:binders"
+    let open_binders = Gram.entry_create "constr:open_binders"
     let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
     let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
     let record_declaration = Gram.entry_create "constr:record_declaration"
@@ -602,10 +604,15 @@ let compute_entry allow_create adjust forpat = function
        else weaken_entry Constr.operconstr),
       adjust (n,q), false
   | ETName -> weaken_entry Prim.name, None, false
+  | ETBinder true -> anomaly "Should occur only as part of BinderList"
+  | ETBinder false -> weaken_entry Constr.binder, None, false
+  | ETBinderList (true,tkl) ->
+      assert (tkl=[]); weaken_entry Constr.open_binders, None, false
+  | ETBinderList (false,_) -> anomaly "List of entries cannot be registered."
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETConstrList _ -> error "List of entries cannot be registered."
+  | ETConstrList _ -> anomaly "List of entries cannot be registered."
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -645,6 +652,12 @@ let is_binder_level from e =
       ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true
     | _ -> false
 
+let make_sep_rules tkl =
+  Gram.srules'
+    [List.map gram_token_of_token tkl,
+     List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
+       (Gram.action (fun loc -> ()))]
+
 let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
   if is_binder_level from typ then
     if forpat then
@@ -660,10 +673,15 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
     | ETConstrList (typ',tkl) ->
         Slist1sep
           (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
-           Gram.srules'
-             [List.map gram_token_of_token tkl,
-              List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
-                (Gram.action (fun loc -> ()))])
+	   make_sep_rules tkl)
+    | ETBinderList (false,[]) ->
+        Slist1
+	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+    | ETBinderList (false,tkl) ->
+        Slist1sep
+	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
+	   make_sep_rules tkl)
+
     | _ ->
     match interp_constr_prod_entry_key assoc from forpat typ with
       | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 99c155e8d..80f4b65fe 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -197,7 +197,9 @@ module Constr :
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
     val closed_binder : local_binder list Gram.entry
-    val binders : local_binder list Gram.entry
+    val binder : local_binder list Gram.entry (* closed_binder or variable *)
+    val binders : local_binder list Gram.entry (* list of binder *)
+    val open_binders : local_binder list Gram.entry
     val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6a4d9757d..e0a8c173a 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -62,8 +62,8 @@ let prec_of_prim_token = function
 
 open Notation
 
-let print_hunks n pr (env,envlist) unp =
-  let env = ref env and envlist = ref envlist in
+let print_hunks n pr pr_binders (terms,termlists,binders) unp =
+  let env = ref terms and envlist = ref termlists and bll = ref binders in
   let pop r = let a = List.hd !r in r := List.tl !r; a in
   let rec aux = function
   | [] -> mt ()
@@ -74,6 +74,8 @@ let print_hunks n pr (env,envlist) unp =
       let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
       let pp2 = aux l in
       pp1 ++ pp2
+  | UnpBinderListMetaVar (_,isopen,sl) :: l ->
+      let cl = pop bll in pr_binders (fun () -> aux sl) isopen cl ++ aux l
   | UnpTerminal s :: l -> str s ++ aux l
   | UnpBox (b,sub) :: l ->
       (* Keep order: side-effects *)
@@ -83,9 +85,9 @@ let print_hunks n pr (env,envlist) unp =
   | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
   aux unp
 
-let pr_notation pr s env =
+let pr_notation pr pr_binders s env =
   let unpl, level = find_notation_printing_rule s in
-  print_hunks level pr env unpl, level
+  print_hunks level pr pr_binders env unpl, level
 
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
@@ -189,7 +191,8 @@ let rec pr_patt sep inh p =
       hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
   | CPatNotation (_,"( _ )",([p],[])) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
+  | CPatNotation (_,s,(l,ll)) ->
+      pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[])
   | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
@@ -252,18 +255,22 @@ let pr_binder_among_many pr_c = function
       hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
-let pr_undelimited_binders pr_c =
-  prlist_with_sep spc (pr_binder_among_many pr_c)
+let pr_undelimited_binders sep pr_c =
+  prlist_with_sep sep (pr_binder_among_many pr_c)
 
-let pr_delimited_binders kw pr_c bl =
+let pr_delimited_binders kw sep pr_c bl =
   let n = begin_of_binders bl in
   match bl with
   | [LocalRawAssum (nal,k,t)] ->
       pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
   | LocalRawAssum _ :: _ as bdl ->
-      pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
+      pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
   | _ -> assert false
 
+let pr_binders_gen pr_c sep is_open =
+  if is_open then pr_delimited_binders mt sep pr_c
+  else pr_undelimited_binders sep pr_c
+
 let rec extract_prod_binders = function
 (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
@@ -318,7 +325,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   let pr_body =
     if dangling_with_for then pr_dangling else pr in
   pr_id id ++ str" " ++
-  hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
+  hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
@@ -438,14 +445,14 @@ let pr pr sep inherited a =
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
       hov 0 (
-	hov 2 (pr_delimited_binders pr_forall
+	hov 2 (pr_delimited_binders pr_forall spc
                  (pr mt ltop) bl) ++
         str "," ++ pr spc ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
       hov 0 (
-        hov 2 (pr_delimited_binders pr_fun
+        hov 2 (pr_delimited_binders pr_fun spc
                 (pr mt ltop) bl) ++
 	  Lazy.force pr_fun_sep ++ pr spc ltop a),
       llambda
@@ -545,9 +552,10 @@ let pr pr sep inherited a =
   | CCast (_,a,CastCoerce) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
       lcast
-  | CNotation (_,"( _ )",([t],[])) ->
+  | CNotation (_,"( _ )",([t],[],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
-  | CNotation (_,s,env) -> pr_notation (pr mt) s env
+  | CNotation (_,s,env) ->
+      pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
   | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
@@ -619,7 +627,7 @@ let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
 
 let pr_cases_pattern_expr = pr_patt ltop
 
-let pr_binders = pr_undelimited_binders (pr ltop)
+let pr_binders = pr_undelimited_binders spc (pr ltop)
 
 let pr_with_occurrences pr occs =
   match occs with
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index dacc2b9b2..503fd734b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -112,7 +112,9 @@ let pr_set_entry_type = function
   | ETConstr _ -> str"constr"
   | ETOther (_,e) -> str e
   | ETBigint -> str "bigint"
-  | ETConstrList _ -> failwith "Internal entry type"
+  | ETBinder true -> str "binder"
+  | ETBinder false -> str "closed binder"
+  | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
 let strip_meta id =
   let s = string_of_id id in
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d78486a0b..20943f143 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -146,11 +146,10 @@ let rec mlexpr_of_constr = function
   | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
   | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Topconstr.CNotation(_,ntn,subst) ->
+  | Topconstr.CNotation(_,ntn,(subst,substl,[])) ->
       <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
-              $mlexpr_of_pair
-                (mlexpr_of_list mlexpr_of_constr)
-                (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >>
+              ($mlexpr_of_list mlexpr_of_constr subst$,
+               $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
   | Topconstr.CPatVar (loc,n) ->
       <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index d84a9d2ed..701c8f707 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -120,7 +120,7 @@ type tomatch_stack = tomatch_status list
      originating from a subterm in which case real args are not dependent;
      it accounts for n+1 binders if dep or n binders if not dep
    - [PrProd] types abstracted term ([Abstract]); it accounts for one binder
-   - [PrCcl] types the right-hand-side
+   - [PrCcl] types the right-hand side
    - Aliases [Alias] have no trace in [predicate_signature]
 *)
 
@@ -1147,7 +1147,7 @@ let rec generalize_problem pb = function
 	  tomatch = Abstract d :: tomatch;
           pred = Option.map (generalize_predicate i d) pb'.pred }
 
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let tycon = match pb.pred with
@@ -1924,7 +1924,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 
   let typing_fun tycon env = typing_fun tycon env isevars in
 
-  (* We build the matrix of patterns and right-hand-side *)
+  (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env eqns in
 
   (* We build the vector of terms to match consistently with the *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index da417f44d..1ae4d96fa 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1032,7 +1032,7 @@ let rec generalize_problem names pb = function
 	  tomatch = Abstract d :: tomatch;
           pred = generalize_predicate names i d pb.tomatch pb'.pred  }
 
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
@@ -1669,7 +1669,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
 
-  (* We build the matrix of patterns and right-hand-side *)
+  (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env tomatchl eqns in
 
   (* We build the vector of terms to match consistently with the *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9113efd55..01d1b8b00 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -362,6 +362,8 @@ let detype_sort = function
   | Prop c -> RProp c
   | Type u -> RType (Some u)
 
+type binder_kind = BProd | BLambda | BLetIn
+
 (**********************************************************************)
 (* Main detyping function                                             *)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index fb6bf8545..6dbaebc46 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,8 +32,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -183,6 +181,36 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
+let fold_rawconstr f acc =
+  let rec fold acc = function
+  | RVar _ -> acc
+  | RApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) ->
+      fold (fold acc b) c
+  | RCases (_,_,rtntypopt,tml,pl) ->
+      List.fold_left fold_pattern
+	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
+	pl
+    | RLetTuple (_,_,rtntyp,b,c) ->
+	fold (fold (fold_return_type acc rtntyp) b) c
+    | RIf (_,c,rtntyp,b1,b2) ->
+	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
+    | RRec (_,_,_,bl,tyl,bv) ->
+	let acc = Array.fold_left
+	  (List.fold_left (fun acc (na,k,bbd,bty) ->
+	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
+	Array.fold_left fold (Array.fold_left fold acc tyl) bv
+    | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc
+
+  and fold_pattern acc (_,idl,p,c) = fold acc c
+
+  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
+
+  in fold acc
+
+let iter_rawconstr f = fold_rawconstr (fun () -> f) ()
+
 let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2498af7b5..242244bd6 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -33,8 +33,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -105,6 +103,8 @@ val map_rawconstr_with_binders_loc : loc ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
 *)
 
+val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a
+val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit
 val occur_rawconstr : identifier -> rawconstr -> bool
 val free_rawvars : rawconstr -> identifier list
 val loc_of_rawconstr : rawconstr -> loc
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 645de69cd..7874f4695 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 924030bac..215d9b68c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,32 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+The command has indeed failed with message:
+=> Error: x should not be bound in a recursive pattern of the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+   term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: The reference w was not found in the current environment.
+The command has indeed failed with message:
+=> Error: x is unbound in the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+   term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: z is expected to occur in binding position in the right-hand side.
+The command has indeed failed with message:
+=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
@@ -59,6 +85,8 @@ Defining 'I' as keyword
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
+[|0 * (1, 2, 3); (4, 5, 6) * false|]
+     : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
 plus
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index f041b9b71..b8f8f48f3 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -121,6 +121,39 @@ Notation "- 4" := (-2 + -2).
 Check -4.
 
 (**********************************************************************)
+(* Check ill-formed recursive notations *)
+
+(* Recursive variables not part of a recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y z) ..).
+
+(* No recursive notation *)
+Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
+
+(* Left-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
+
+(* Right-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+
+(* Not the right kind of recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
+Fail Notation "( x -- y , .. , z )" := (pair y .. (pair z 0) ..)
+  (y closed binder, z closed binder).
+
+(* No separator allowed with open binders *)
+Fail Notation "( x -- y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..))
+  (y binder, z binder).
+
+(* Ends of pattern do not match *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair (plus z) 0) ..).
+Fail Notation "( x , y , .. , z )" := (pair y .. (plus z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (y y .. (x2 z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (x1 y .. (x2 z 0) ..).
+
+(* Ends of pattern are the same *)
+Fail Notation "( x , y , .. , z )" := (pair .. (pair (pair y z) x) .. x).
+
+(**********************************************************************)
 (* Check preservation of scopes at printing time *)
 
 Notation SUM := sum.
@@ -163,6 +196,12 @@ Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
   (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
 Check [|1,2,3;4,5,6|].
 
+Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
+  (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
+        (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
+  (t at level 39).
+Check [|0*(1,2,3);(4,5,6)*false|].
+
 (**********************************************************************)
 (* Test recursive notations involving applications                    *)
 (* Caveat: does not work for applied constant because constants are   *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 20d20d826..6731d5054 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,3 +10,18 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
+∃ n p : nat, n + p = 0
+     : Prop
+∀ n p : nat, n + p = 0
+     : Prop
+λ n p : nat, n + p = 0
+     : nat -> nat -> Prop
+λ (A : Type) (n p : A), n = p
+     : ∀ A : Type, A -> A -> Prop
+λ A : Type, ∃ n p : A, n = p
+     : Type -> Prop
+λ A : Type, ∀ n p : A, n = p
+     : Type -> Prop
+Defining 'let'' as keyword
+let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+     : bool -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 2e136edf1..57d8ebbc4 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -24,3 +24,44 @@ Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
 Remove Printing Let prod.
 Check match (0,0,0) with (x,y,z) => x+y+z end.
 Check let '(a,b,c) := ((2,3),4) in a.
+
+(* Test notations with binders *)
+
+Notation "∃  x .. y , P":=
+  (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+
+Check (∃ n p, n+p=0).
+
+Notation "∀  x .. y , P":= (forall x, .. (forall y, P) ..)
+  (x binder, at level 200, right associativity).
+
+Check (∀ n p, n+p=0).
+
+Notation "'λ'  x .. y , P":= (fun x, .. (fun y, P) ..)
+  (y binder, at level 200, right associativity).
+
+Check (λ n p, n+p=0).
+
+Generalizable Variable A.
+
+Check `(λ n p : A, n=p).
+Check `(∃ n p : A, n=p).
+Check `(∀ n p : A, n=p).
+
+Notation "'let'' f x .. y  :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (f ident, x closed binder, y closed binder, at level 200,
+   right associativity).
+
+Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
+
+(* This one is not fully satisfactory because binders in the same type
+   are re-factorized and parentheses are needed even for atomic binder
+
+Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (f ident, x closed binder, y closed binder, at level 200,
+   right associativity).
+
+Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
+*)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6dda11405..f438073be 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -280,7 +280,7 @@ let rec find_pattern nt xl = function
   | [], NonTerminal x' :: l' ->
       (out_nt nt,x',List.rev xl),l'
   | _, Terminal s :: _ | Terminal s :: _, _ ->
-      error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
+      error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
@@ -289,23 +289,23 @@ let rec find_pattern nt xl = function
       anomaly "Only Terminal or Break expected on left, non-SProdList on right"
 
 let rec interp_list_parser hd = function
-  | [] -> [], [], List.rev hd
+  | [] -> [], List.rev hd
   | NonTerminal id :: tl when id = ldots_var ->
       let hd = List.rev hd in
       let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
-      let yl,xl,tl'' = interp_list_parser [] tl' in
+      let xyl,tl'' = interp_list_parser [] tl' in
       (* We remember each pair of variable denoting a recursive part to *)
       (* remove the second copy of it afterwards *)
-      (y,x)::yl, x::xl, SProdList (x,sl) :: tl''
+      (x,y)::xyl, SProdList (x,sl) :: tl''
   | (Terminal _ | Break _) as s :: tl ->
       if hd = [] then
-        let yl,xl,tl' = interp_list_parser [] tl in
-        yl, xl, s :: tl'
+        let yl,tl' = interp_list_parser [] tl in
+        yl, s :: tl'
       else
         interp_list_parser (s::hd) tl
   | NonTerminal _ as x :: tl ->
-      let yl,xl,tl' = interp_list_parser [x] tl in
-      yl, xl, List.rev_append hd tl'
+      let xyl,tl' = interp_list_parser [x] tl in
+      xyl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
 
@@ -345,33 +345,28 @@ let rec get_notation_vars = function
   | [] -> []
   | NonTerminal id :: sl ->
       let vars = get_notation_vars sl in
-      if List.mem id vars then
-        if id <> ldots_var then
+      if id = ldots_var then vars else
+	if List.mem id vars then
 	  error ("Variable "^string_of_id id^" occurs more than once.")
-        else
-          vars
-      else
-        id::vars
+	else
+          id::vars
   | (Terminal _ | Break _) :: sl -> get_notation_vars sl
   | SProdList _ :: _ -> assert false
 
 let analyze_notation_tokens l =
   let l = raw_analyze_notation_tokens l in
   let vars = get_notation_vars l in
-  let extrarecvars,recvars,l = interp_list_parser [] l in
-  (if extrarecvars = [] then [], [], vars, l
-   else extrarecvars, recvars, list_subtract vars recvars, l)
-
-let remove_extravars extrarecvars (vars,recvars) =
-  let vars =
-    List.fold_right (fun (x,y) l ->
-      if List.assoc x l <> List.assoc y recvars then
-	error
-	 "Two end variables of a recursive notation are not in the same scope."
-      else
-	List.remove_assoc x l)
-      extrarecvars (List.remove_assoc ldots_var vars) in
-  (vars,recvars)
+  let recvars,l = interp_list_parser [] l in
+  recvars, list_subtract vars (List.map snd recvars), l
+
+let error_not_same_scope x y =
+  error ("Variables "^string_of_id x^" and "^string_of_id y^
+    " must be in the same scope.")
+
+let error_both_bound_and_binding x y =
+  errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++
+  strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder
+  for both terms and binders.")
 
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
@@ -434,6 +429,13 @@ let rec is_non_terminal = function
 
 let add_break n l = UnpCut (PpBrk(n,0)) :: l
 
+let check_open_binder isopen sl m =
+  if isopen & sl <> [] then
+    errorlabstrm "" (str "as " ++ pr_id m ++
+      str " is a non-closed binder, no such \"" ++
+      prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+      ++ strbrk "\" is allowed to occur.")
+
 (* Heuristics for building default printing rules *)
 
 type previous_prod_status = NoBreak | CanBreak
@@ -478,7 +480,7 @@ let make_hunks etyps symbols from =
 
     | Terminal s :: prods ->
 	if is_right_bracket s then
-	  UnpTerminal s ::make NoBreak prods
+	  UnpTerminal s :: make NoBreak prods
         else if ws = CanBreak then
 	  add_break 1 (UnpTerminal s :: make NoBreak prods)
         else
@@ -489,14 +491,20 @@ let make_hunks etyps symbols from =
 
     | SProdList (m,sl) :: prods ->
 	let i = list_index m vars in
-	let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+	let typ = List.nth typs (i-1) in
+	let _,prec = precedence_of_entry_type from typ in
         let sl' =
           (* If no separator: add a break *)
 	  if sl = [] then add_break 1 []
           (* We add NonTerminal for simulation but remove it afterwards *)
-	  else snd (list_sep_last (make NoBreak (sl@[NonTerminal m])))
-	in
-	UnpListMetaVar (i,prec,sl') :: make CanBreak prods
+	  else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) in
+	let hunk = match typ with
+	  | ETConstr _ -> UnpListMetaVar (i,prec,sl')
+	  | ETBinder isopen ->
+	      check_open_binder isopen sl m;
+	      UnpBinderListMetaVar (i,isopen,sl')
+	  | _ -> assert false in
+	hunk :: make CanBreak prods
 
     | [] -> []
 
@@ -559,12 +567,19 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | SProdList (m,sl) :: symbs, fmt ->
       let i = list_index m vars in
-      let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+      let typ = List.nth typs (i-1) in
+      let _,prec = precedence_of_entry_type from typ in
       let slfmt,fmt = read_recursive_format sl fmt in
       let sl, slfmt = aux (sl,slfmt) in
       if sl <> [] then error_format ();
       let symbs, l = aux (symbs,fmt) in
-      symbs, UnpListMetaVar (i,prec,slfmt) :: l
+      let hunk = match typ with
+	| ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+	| ETBinder isopen ->
+	    check_open_binder isopen sl m;
+	    UnpBinderListMetaVar (i,isopen,slfmt)
+	| _ -> assert false in
+      symbs, hunk :: l
   | symbs, [] -> symbs, []
   | _, _ -> error_format ()
   in
@@ -632,11 +647,13 @@ let make_production etyps symbols =
               (List.map (function Terminal s -> [terminal s]
                 | Break _ -> []
                 | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
-	    let typ = match List.assoc x etyps with
-              | ETConstr x -> x
-              | _ ->
-                  error "Component of recursive patterns in notation must be constr." in
-	    expand_list_rule typ tkl x 1 0 [] ll)
+	    match List.assoc x etyps with
+            | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll
+            | ETBinder o ->
+		distribute
+                  [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll
+            | _ ->
+                error "Components of recursive patterns in notation must be terms or binders.")
       symbols [[]] in
   List.map define_keywords prod
 
@@ -682,7 +699,7 @@ let error_incompatible_level ntn oldprec prec =
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
 
-let cache_one_syntax_extension (prec,ntn,gr,pp) =
+let cache_one_syntax_extension (typs,prec,ntn,gr,pp) =
   try
     let oldprec = Notation.level_of_notation ntn in
     if prec <> oldprec then error_incompatible_level ntn oldprec prec
@@ -690,7 +707,7 @@ let cache_one_syntax_extension (prec,ntn,gr,pp) =
     (* Reserve the notation level *)
     Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
-    Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
+    Egrammar.extend_grammar (Egrammar.Notation (prec,typs,gr));
     (* Declare the printing rule *)
     Notation.declare_notation_printing_rule ntn (pp,fst prec)
 
@@ -702,8 +719,9 @@ let subst_parsing_rule subst x = x
 let subst_printing_rule subst x = x
 
 let subst_syntax_extension (subst,(local,sy)) =
-  (local, List.map (fun (prec,ntn,gr,pp) ->
-     (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy)
+  (local, List.map (fun (typs,prec,ntn,gr,pp) ->
+     (typs,prec,ntn,subst_parsing_rule subst gr,subst_printing_rule subst pp))
+    sy)
 
 let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
@@ -768,11 +786,59 @@ let set_entry_type etyps (x,typ) =
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
           ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
-      | (ETPattern | ETName | ETBigint | ETOther _ | ETReference as t), _ -> t
-      | (ETConstrList _, _) -> assert false
+      | (ETPattern | ETName | ETBigint | ETOther _ |
+	 ETReference | ETBinder _ as t), _ -> t
+      | (ETBinderList _ |ETConstrList _), _ -> assert false
     with Not_found -> ETConstr typ
   in (x,typ)
 
+let join_auxiliary_recursive_types recvars etyps =
+  List.fold_right (fun (x,y) typs ->
+    let xtyp = try Some (List.assoc x etyps) with Not_found -> None in
+    let ytyp = try Some (List.assoc y etyps) with Not_found -> None in
+    match xtyp,ytyp with
+    | None, None -> typs
+    | Some _, None -> typs
+    | None, Some ytyp -> (x,ytyp)::typs
+    | Some xtyp, Some ytyp when xtyp = ytyp -> typs
+    | Some xtyp, Some ytyp ->
+	errorlabstrm ""
+	  (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
+	   strbrk ", both ends have incompatible types."))
+    recvars etyps
+
+let internalization_type_of_entry_type = function
+  | ETConstr _ -> NtnInternTypeConstr
+  | ETBigint | ETReference -> NtnInternTypeConstr
+  | ETBinder _ -> NtnInternTypeBinder
+  | ETName -> NtnInternTypeIdent
+  | ETPattern | ETOther _ -> error "Not supported."
+  | ETBinderList _ | ETConstrList _ -> assert false
+
+let set_internalization_type typs =
+  List.map (down_snd internalization_type_of_entry_type) typs
+
+let make_internalization_vars recvars mainvars typs =
+  let maintyps = List.combine mainvars typs in
+  let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
+  maintyps@extratyps
+
+let make_interpretation_type isrec = function
+  | NtnInternTypeConstr when isrec -> NtnTypeConstrList
+  | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
+  | NtnInternTypeBinder when isrec -> NtnTypeBinderList
+  | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
+
+let make_interpretation_vars recvars allvars =
+  List.iter (fun (x,y) ->
+    if fst (List.assoc x allvars) <> fst (List.assoc y allvars) then
+      error_not_same_scope x y) recvars;
+  let useless_recvars = List.map snd recvars in
+  let mainvars =
+    List.filter (fun (x,_) -> not (List.mem x useless_recvars)) allvars in
+  List.map (fun (x,(sc,typ)) ->
+    (x,(sc,make_interpretation_type (List.mem_assoc x recvars) typ))) mainvars
+
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
     error "A notation must include at least one symbol.";
@@ -791,29 +857,31 @@ let find_precedence lev etyps symbols =
 	    error "The level of the leftmost non-terminal cannot be changed."
 	| ETName | ETBigint | ETReference ->
 	    if lev = None then
-	      if_verbose msgnl (str "Setting notation at level 0.")
+	      ([msgnl,str "Setting notation at level 0."],0)
 	    else
 	    if lev <> Some 0 then
-	      error "A notation starting with an atomic expression must be at level 0.";
-	    0
-	| ETPattern | ETOther _ -> (* Give a default ? *)
+	      error "A notation starting with an atomic expression must be at level 0."
+	    else
+	      ([],0)
+	| ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
 	    if lev = None then
 	      error "Need an explicit level."
-	    else Option.get lev
-        | ETConstrList _ -> assert false (* internally used in grammar only *)
+	    else [],Option.get lev
+        | ETConstrList _ | ETBinderList _ ->
+	    assert false (* internally used in grammar only *)
       with Not_found ->
 	if lev = None then
 	  error "A left-recursive notation must have an explicit level."
-	else Option.get lev)
+	else [],Option.get lev)
   | Terminal _ ::l when
       (match list_last symbols with Terminal _ -> true |_ -> false)
       ->
       if lev = None then
-	(if_verbose msgnl (str "Setting notation at level 0."); 0)
-      else Option.get lev
+	([msgnl,str "Setting notation at level 0."], 0)
+      else [],Option.get lev
   | _ ->
       if lev = None then error "Cannot determine the level.";
-      Option.get lev
+      [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notation.level_of_notation "{ _ }" in ()
@@ -846,16 +914,15 @@ let remove_curly_brackets l =
 
 let compute_syntax_data (df,modifiers) =
   let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
-  (* Notation defaults to NONA *)
-  let assoc = match assoc with None -> Some NonA | a -> a in
+  let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
   let toks = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
   let ntn_for_interp = make_notation_key symbols in
   let symbols' = remove_curly_brackets symbols in
   let need_squash = (symbols <> symbols') in
   let ntn_for_grammar = make_notation_key symbols' in
   check_rule_productivity symbols';
-  let n = find_precedence n etyps symbols' in
+  let msgs,n = find_precedence n etyps symbols' in
   let innerlevel = NumLevel 200 in
   let typs =
     find_symbols
@@ -864,12 +931,25 @@ let compute_syntax_data (df,modifiers) =
       (NumLevel n,BorderProd(Right,assoc))
       symbols' in
   (* To globalize... *)
-  let typs = List.map (set_entry_type etyps) typs in
-  let prec = (n,List.map (assoc_of_type n) typs) in
-  let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
+  let etyps = join_auxiliary_recursive_types recvars etyps in
+  let sy_typs = List.map (set_entry_type etyps) typs in
+  let prec = (n,List.map (assoc_of_type n) sy_typs) in
+  let i_typs = set_internalization_type sy_typs in
+  let sy_data = (n,sy_typs,symbols',fmt) in
+  let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
-  let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
-  (i_data,sy_data)
+  let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
+  (* Return relevant data for interpretation and for parsing/printing *)
+  (msgs,i_data,i_typs,sy_fulldata)
+
+let compute_pure_syntax_data (df,mods) =
+  let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data (df,mods) in
+  let msgs =
+    if onlyparse then
+      (msg_warning,
+      str "The only parsing modifier has no effect in Reserved Notation.")::msgs
+    else msgs in
+  msgs, sy_data
 
 (**********************************************************************)
 (* Registration of notations interpretation                            *)
@@ -925,9 +1005,9 @@ exception NoSyntaxRule
 let recover_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
-    let pprule,_ = Notation.find_notation_printing_rule ntn in
-    let gr = Egrammar.recover_notation_grammar ntn prec in
-    (prec,ntn,gr,pprule)
+    let pp_rule,_ = Notation.find_notation_printing_rule ntn in
+    let typs,pa_rule = Egrammar.recover_notation_grammar ntn prec in
+    (typs,prec,ntn,pa_rule,pp_rule)
   with Not_found ->
     raise NoSyntaxRule
 
@@ -935,9 +1015,9 @@ let recover_squash_syntax () = recover_syntax "{ _ }"
 
 let recover_notation_syntax rawntn =
   let ntn = contract_notation rawntn in
-  let sy_rule = recover_syntax ntn in
+  let (typs,_,_,_,_ as sy_rule) = recover_syntax ntn in
   let need_squash = ntn<>rawntn in
-  if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
+  typs,if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
@@ -952,10 +1032,10 @@ let make_pp_rule (n,typs,symbols,fmt) =
   | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
   | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt)
 
-let make_syntax_rules (ntn,prec,need_squash,sy_data) =
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
   let pa_rule = make_pa_rule sy_data ntn in
   let pp_rule = make_pp_rule sy_data in
-  let sy_rule = (prec,ntn,pa_rule,pp_rule) in
+  let sy_rule = (i_typs,prec,ntn,pa_rule,pp_rule) in
   (* By construction, the rule for "{ _ }" is declared, but we need to
      redeclare it because the file where it is declared needs not be open
      when the current file opens (especially in presence of -nois) *)
@@ -965,31 +1045,35 @@ let make_syntax_rules (ntn,prec,need_squash,sy_data) =
 (* Main functions about notations                                     *)
 
 let add_notation_in_scope local df c mods scope =
-  let (i_data,sy_data) = compute_syntax_data (df,mods) in
-  (* Declare the parsing and printing rules *)
+  let (msgs,i_data,i_typs,sy_data) = compute_syntax_data (df,mods) in
+  (* Prepare the parsing and printing rules *)
   let sy_rules = make_syntax_rules sy_data in
-  Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
-  (* Declare interpretation *)
-  let (onlyparse,extrarecvars,recvars,vars,df') = i_data in
-  let (acvars,ac) = interp_aconstr (vars,recvars) c in
-  let a = (remove_extravars extrarecvars acvars,ac) in
+  (* Prepare the interpretation *)
+  let (onlyparse,recvars,mainvars,df') = i_data in
+  let i_vars = make_internalization_vars recvars mainvars i_typs in
+  let (acvars,ac) = interp_aconstr i_vars recvars c in
+  let a = (make_interpretation_vars recvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
+  (* Ready to change the global state *)
+  Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
+  Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
   Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
   df'
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
   let dfs = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in
-  (* Redeclare pa/pp rules *)
-  if not (is_numeral symbs) then begin
-    let sy_rules = recover_notation_syntax (make_notation_key symbs) in
-    Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
-  end;
+  let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
+  (* Recover types of variables and pa/pp rules; redeclare them if needed *)
+  let i_typs = if not (is_numeral symbs) then begin
+    let i_typs,sy_rules = recover_notation_syntax (make_notation_key symbs) in
+    Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)); i_typs
+  end else [] in
   (* Declare interpretation *)
   let path = (Lib.library_dp(),Lib.current_dirpath true) in
   let df' = (make_notation_key symbs,(path,df)) in
-  let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in
-  let a = (remove_extravars extrarecvars acvars,ac) in
+  let i_vars = make_internalization_vars recvars mainvars i_typs in
+  let (acvars,ac) = interp_aconstr ~impls i_vars recvars c in
+  let a = (make_interpretation_vars recvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
   Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
   df'
@@ -997,8 +1081,9 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
 (* Notations without interpretation (Reserved Notation) *)
 
 let add_syntax_extension local ((loc,df),mods) =
-  let (_,sy_data) = compute_syntax_data (df,mods) in
+  let msgs,sy_data = compute_pure_syntax_data (df,mods) in
   let sy_rules = make_syntax_rules sy_data in
+  Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
@@ -1090,7 +1175,10 @@ let try_interp_name_alias = function
 let add_syntactic_definition ident (vars,c) local onlyparse =
   let vars,pat =
     try [], ARef (try_interp_name_alias (vars,c))
-    with Not_found -> let (vars,_),pat = interp_aconstr (vars,[]) c in vars,pat
+    with Not_found ->
+      let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in
+      let vars,pat = interp_aconstr i_vars [] c in
+      List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
   in
   let onlyparse = onlyparse or is_not_printable pat in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a1eff333..05795566a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1054,7 +1054,7 @@ let vernac_global_check c =
 
 let vernac_print = function
   | PrintTables -> print_tables ()
-  | PrintFullContext -> msg (print_full_context_typ ())
+  | PrintFullContext-> msg (print_full_context_typ ())
   | PrintSectionContext qid -> msg (print_sec_context_typ qid)
   | PrintInspect n -> msg (inspect n)
   | PrintGrammar ent -> Metasyntax.print_grammar ent