Ajout d'abbréviations/notations paramétriques

Example: "Notation reflexive R := (forall x, R x x)."



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

16 files changed, 296 insertions, 262 deletions

diff --git a/CHANGES b/CHANGES
index 8b2078682..ffa6fecb4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -88,6 +88,7 @@ Notations and implicit arguments
 - New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
 - Level "constr" moved from 9 to 8.
 - Structure/Record now printed as Record (unless option Printing All is set).
+- Support for parametric notations defining constants (i.e. abbreviations).
 
 Tactic Language
 
@@ -409,7 +410,8 @@ Libraries
   digit 0; weaken premises in Z_lt_induction).
 - Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
 - Znumtheory now contains a gcd function that can compute within Coq.
-- More lemmas stated on Type in Wf.v, removal of redundant Fix_F.
+- More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and 
+  Acc_iter2.
 - Change of the internal names of lemmas in OmegaLemmas.
 - Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
   the allowance for recursively non uniform parameters (possible
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 583e4406c..dcac68f1a 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -928,35 +928,38 @@ It also displays the lonely notations.
 \label{Abbreviations}
 \comindex{Notation}}
 
-An {\em abbreviation} is a name denoting a (presumably) more complex
-expression. An abbreviation is a special form of notation with no
-parameter and only one symbol which is an identifier. This identifier
-is given with no quotes around. Example:
+An {\em abbreviation} is a name, possibly applied to arguments, that
+denotes a (presumably) more complex expression. Here are examples:
 
 \begin{coq_eval}
 Require Import List.
+Require Import Relations.
+Set Printing Notations.
 \end{coq_eval}
-\begin{coq_example*}
-Notation List := (list nat).
-\end{coq_example*}
+\begin{coq_example}
+Notation Nlist := (list nat).
+Check 1 :: 2 :: 3 :: nil.
+Notation reflexive R := (forall x, R x x).
+Check forall A:Prop, A <-> A.
+Check reflexive iff.
+\end{coq_example}
 
-An abbreviation expects no precedence nor associativity, since it can
-always be put at the lower level of atomic expressions, and
-associativity is irrelevant. Abbreviations are used as much as
-possible by the {\Coq} printers unless the modifier
+An abbreviation expects no precedence nor associativity, since it
+follows the usual syntax of application. Abbreviations are used as
+much as possible by the {\Coq} printers unless the modifier
 \verb=(only parsing)= is given.
 
-Abbreviations are bound to an absolute name like for an ordinary
-definition, and can be referred by partially qualified names too.
+Abbreviations are bound to an absolute name as an ordinary
+definition is, and they can be referred by qualified names too.
 
 Abbreviations are syntactic in the sense that they are bound to
 expressions which are not typed at the time of the definition of the
-abbreviation but at the time it is used. Especially, abbreviation can
+abbreviation but at the time it is used. Especially, abbreviations can
 be bound to terms with holes (i.e. with ``\_''). The general syntax
 for abbreviations is
 \begin{quote}
-\texttt{Notation} \zeroone{{\tt Local}} {\ident} \texttt{:=} {\term} 
- \zeroone{{\tt (only parsing)}} \verb=.=
+\texttt{Notation} \zeroone{{\tt Local}} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
+ \zeroone{{\tt (only parsing)}}~\verb=.=
 \end{quote}
 
 \Example
@@ -974,11 +977,11 @@ Abbreviations do not survive the end of sections. No typing of the denoted
 expression is performed at definition time. Type-checking is done only
 at the time of use of the abbreviation.
 
-\Rem \index{Syntactic Definition} % For
-compatibility Abbreviations are similar to the {\em syntactic
-definitions} available in versions of {\Coq} prior to version 8.0,
-except that abbreviations are used for printing (unless the modifier
-\verb=(only parsing)= is given) while syntactic definitions were not.
+%\Rem \index{Syntactic Definition} %
+%Abbreviations are similar to the {\em syntactic
+%definitions} available in versions of {\Coq} prior to version 8.0,
+%except that abbreviations are used for printing (unless the modifier
+%\verb=(only parsing)= is given) while syntactic definitions were not.
 
 \section{Tactic Notations}
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 11cd87763..0e30e5db5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -853,7 +853,12 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                       subst in
 	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
-              CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
+	      let l =
+		List.map (fun (c,(scopt,scl)) ->
+		  extern true (scopt,scl@scopes) vars c, None)
+		  subst 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 
 	else
 	  (* TODO: compute scopt for the extra args, in case, head is a ref *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9e962267d..a0e9b6bb5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -234,6 +234,92 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
     idscopes := Some (scopt,scopes)
 
 (**********************************************************************)
+(* Syntax extensions                                                  *)
+
+let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
+  try
+    (* Binders bound in the notation are considered first-order objects *)
+    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
+    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
+  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.map snd renaming in
+    let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
+    let id' = next_ident_away id fvs in
+    let renaming' = if id=id' then renaming else (id,id')::renaming in
+    (renaming',env), id'
+
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+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 (renaming,(ids,_,scopes)) =
+  function
+  | 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,scopt,subscopes@scopes) a
+	with Not_found -> 
+	try 
+	  RVar (loc,List.assoc id renaming)
+	with Not_found -> 
+	  (* Happens for local notation joint with inductive/fixpoint defs *)
+	  RVar (loc,id)
+      end
+  | AList (x,_,iter,terminator,lassoc) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let termin = 
+          subst_aconstr_in_rawconstr loc interp subst 
+	    (renaming,(ids,None,scopes)) terminator in
+        let l = decode_constrlist_value a in
+	List.fold_right (fun a t -> 
+          subst_iterator ldots_var t
+            (subst_aconstr_in_rawconstr loc interp 
+              ((x,(a,(scopt,subscopes)))::subst)
+	      (renaming,(ids,None,scopes)) iter))
+            (if lassoc then List.rev l else l) termin
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
+  | t ->
+      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+      (subst_aconstr_in_rawconstr loc interp subst)
+      (renaming,(ids,None,scopes)) t
+
+let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
+  let ntn,args = contract_notation ntn args in
+  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+  if !dump then dump_notation_location (ntn_loc loc args ntn) df;
+  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+  subst_aconstr_in_rawconstr loc intern subst ([],env) c
+
+let set_type_scope (ids,tmp_scope,scopes) =
+  (ids,Some Notation.type_scope,scopes)
+
+let reset_tmp_scope (ids,tmp_scope,scopes) =
+  (ids,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
+
+(**********************************************************************)
 (* Discriminating between bound variables and global references       *)
 
 (* [vars1] is a set of name to avoid (used for the tactic language);
@@ -281,52 +367,59 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
+let error_not_enough_arguments loc =
+  user_err_loc (loc,"",str "Abbreviation is not applied enough")
+
+let check_no_explicitation l =
+  let l = List.filter (fun (a,b) -> b <> None) l in
+  if l <> [] then
+    let loc = fst (Option.get (snd (List.hd l))) in
+    user_err_loc
+      (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid =
+let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
       if !dump then add_glob loc ref;
-      RRef (loc, ref)
+      RRef (loc, ref), args
   | SyntacticDef sp ->
-      Syntax_def.search_syntactic_definition loc sp
+      let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
+      let nids = List.length ids in
+      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
   with Not_found ->
     error_global_not_found_loc loc qid
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid =
-  match intern_qualid loc qid with
-    | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid
+let intern_non_secvar_qualid loc qid intern env args =
+  match intern_qualid loc qid intern env args with
+    | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
     | r -> r
 
-let intern_inductive r =
-  let loc,qid = qualid_of_reference r in
-  try match Nametab.extended_locate qid with
-  | TrueGlobal (IndRef ind) -> ind, []
-  | TrueGlobal _ -> raise Not_found
-  | SyntacticDef sp ->
-      (match Syntax_def.search_syntactic_definition loc sp with
-	| RApp (_,RRef(_,IndRef ind),l)
-	    when List.for_all (function RHole _ -> true | _ -> false) l ->
-	    (ind, List.map (fun _ -> Anonymous) l)
-	| _ -> raise Not_found)
-  with Not_found ->
-    error_global_not_found_loc loc qid
-
-let intern_reference env lvar = function
+let intern_applied_reference intern env lvar args = function
   | Qualid (loc, qid) ->
-      find_appl_head_data lvar (intern_qualid loc qid)
+      let r,args2 = intern_qualid loc qid intern env args in
+      find_appl_head_data lvar r, args2
   | Ident (loc, id) ->
-      try intern_var env lvar loc id
+      try intern_var env lvar loc id,args
       with Not_found -> 
       let qid = make_short_qualid id in
-      try find_appl_head_data lvar (intern_non_secvar_qualid loc qid)
+      try
+	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
+	find_appl_head_data lvar r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
-	if !interning_grammar then RVar (loc,id), [], [], []
+	if !interning_grammar then (RVar (loc,id), [], [], []),args
 	else raise e
 
 let interp_reference vars r =
-  let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r 
+  let (r,_,_,_),_ =
+    intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
+      (Idset.empty,None,[]) (vars,[],[],([],[])) [] r
   in r
 
 let apply_scope_env (ids,_,scopes) = function
@@ -339,10 +432,17 @@ let rec adjust_scopes env scopes = function
       let (enva,scopes) = apply_scope_env env scopes in
       enva :: adjust_scopes env scopes args
 
-let rec simple_adjust_scopes = function
-  | _,[] -> []
-  | [],_::args -> None :: simple_adjust_scopes ([],args)
-  | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args)
+let rec simple_adjust_scopes n = function
+  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+  | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
+
+let find_remaining_constructor_scopes pl1 (ind,j as cstr) =
+  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  let npar = mib.Declarations.mind_nparams in
+  let nargs = Declarations.recarg_length mip.Declarations.mind_recargs j in
+  snd (list_chop (List.length pl1 + npar)
+    (simple_adjust_scopes (npar+nargs)
+      (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
 (* Cases                                                              *)
@@ -411,6 +511,16 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
+let error_invalid_pattern_notation loc =
+  user_err_loc (loc,"",str "Invalid notation for pattern")
+
+let chop_aconstr_constructor loc (ind,k) args =
+  let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let params,args = list_chop nparams args in
+  List.iter (function AHole _ -> ()
+    | _ -> error_invalid_pattern_notation loc) params;
+  args
+
 let decode_patlist_value = function
   | CPatCstr (_,_,l) -> l
   | _ -> anomaly "Ill-formed list argument of notation"
@@ -444,13 +554,12 @@ let subst_cases_pattern loc alias intern subst scopes a =
       end
   | ARef (ConstructRef c) ->
       ([],[[], PatCstr (loc,c, [], alias)])
-  | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
-      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let _,args = list_chop nparams args in
+  | AApp (ARef (ConstructRef cstr),args) ->
+      let args = chop_aconstr_constructor loc cstr args in
       let idslpll = List.map (aux Anonymous subst) args in
       let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (subst,pl) -> 
-        subst,PatCstr (loc,c,pl,alias)) pll in
+        subst,PatCstr (loc,cstr,pl,alias)) pll in
 	ids', pl'
   | AList (x,_,iter,terminator,lassoc) ->
       (try 
@@ -468,65 +577,57 @@ let subst_cases_pattern loc alias intern subst scopes a =
 	  match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found -> 
           anomaly "Inconsistent substitution of recursive notation")
-  | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
+  | t -> error_invalid_pattern_notation loc
   in aux alias subst a
     
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
-  | ConstrPat of (constructor * cases_pattern list)
+  | ConstrPat of constructor * (identifier list * 
+      ((identifier * identifier) list * cases_pattern) list) list
   | VarPat of identifier
 
-let rec patt_of_rawterm loc cstr =
-  match cstr with
-    | RRef (_,(ConstructRef c as x)) ->
-	if !dump then add_glob loc x; 
- 	(c,[])
-    | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
-    | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
-        if !dump then add_glob loc x;
-        let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
-        let npar = mib.Declarations.mind_nparams in
-        let (params,args) =
-          if List.length pl <= npar then (pl,[]) else
-            list_chop npar pl in
-        (* All parameters must be _ *)
-        List.iter
-          (function RHole _ -> ()
-            | _ -> raise Not_found) params;
-        let pl' = List.map
-          (fun c ->
-            let (c,pl) = patt_of_rawterm loc c in
-            PatCstr(loc,c,pl,Anonymous)) args in
-        (c,pl')
-    | _ -> raise Not_found
-
-let find_constructor ref =
+let find_constructor ref f aliases pats scopes =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
     try extended_locate qid
-    with Not_found ->
-      raise (InternalisationError (loc,NotAConstructor ref)) in
-    match gref with
-      | SyntacticDef sp ->
-          let sdef = Syntax_def.search_syntactic_definition loc sp in
-            patt_of_rawterm loc sdef
-      | TrueGlobal r ->
-          let rec unf = function
-            | ConstRef cst ->
-		let v = Environ.constant_value (Global.env()) cst in
-		  unf (global_of_constr v)
-            | ConstructRef c -> 
-		if !dump then add_glob loc r; 
-		c, []
-            | _ -> raise Not_found
-          in unf r
+    with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
+  match gref with
+  | SyntacticDef sp ->
+      let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+      (match a with
+       | ARef (ConstructRef cstr) ->
+	   assert (vars=[]);
+	   cstr, [], pats
+       | AApp (ARef (ConstructRef cstr),args) ->
+	   let args = chop_aconstr_constructor loc cstr args in
+	   let nvars = List.length vars in
+	   if List.length pats < nvars then error_not_enough_arguments loc;
+	   let pats1,pats2 = list_chop nvars pats in
+	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
+	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in
+	   cstr, idspl1, pats2
+       | _ -> error_invalid_pattern_notation loc)
+      
+  | TrueGlobal r ->
+      let rec unf = function
+        | ConstRef cst ->
+	    let v = Environ.constant_value (Global.env()) cst in
+	    unf (global_of_constr v)
+        | ConstructRef cstr -> 
+	    if !dump then add_glob loc r; 
+	    cstr, [], pats
+        | _ -> raise Not_found
+      in unf r
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
 
-let maybe_constructor ref =
-  try ConstrPat (find_constructor ref)
+let maybe_constructor ref f aliases scopes =
+  try
+    let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
+    assert (pl2 = []);
+    ConstrPat (c,idspl1)
   with
       (* patt var does not exists globally *)
     | InternalisationError _ -> VarPat (find_pattern_variable ref)
@@ -536,39 +637,37 @@ let maybe_constructor ref =
               str " is understood as a pattern variable");
         VarPat (find_pattern_variable ref)
 
-let mustbe_constructor loc ref = 
-  try find_constructor ref
+let mustbe_constructor loc ref f aliases patl scopes = 
+  try find_constructor ref f aliases patl scopes
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalisationError (loc,NotAConstructor ref))
 
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = 
-  function
+let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+  let intern_pat = intern_cases_pattern genv in 
+  match pat with
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
-      intern_cases_pattern genv scopes aliases' tmp_scope p
+      intern_pat scopes aliases' tmp_scope p
   | CPatCstr (loc, head, pl) ->
-      let c,pl0 = mustbe_constructor loc head in
-      let argscs =
-	simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
-      check_constructor_length genv loc c pl0 pl;
-      let idslpl =
-	List.map2 (intern_cases_pattern genv scopes ([],[])) argscs pl in
-      let (ids',pll) = product_of_cases_patterns ids idslpl in
+      let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
+      check_constructor_length genv loc c idslpl1 pl2;
+      let argscs2 = find_remaining_constructor_scopes idslpl1 c in
+      let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
+      let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
       let pl' = List.map (fun (subst,pl) ->
-        (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in
+        (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
       ids',pl'
   | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)]) 
       when Bigint.is_strictly_pos p ->
-      let np = Numeral (Bigint.neg p) in
-      intern_cases_pattern genv scopes aliases tmp_scope (CPatPrim(loc,np))
+      intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
   | CPatNotation (_,"( _ )",[a]) ->
-      intern_cases_pattern genv scopes aliases tmp_scope a
+      intern_pat scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
-      let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes 
+      let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
@@ -578,13 +677,14 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       if !dump then dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
-      intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
-        aliases None e
+      intern_pat (find_delimiters_scope loc key::scopes) aliases None e
   | CPatAtom (loc, Some head) ->
-      (match maybe_constructor head with
-	 | ConstrPat (c,args) ->
-	     check_constructor_length genv loc c [] [];
-	     (ids,[subst, PatCstr (loc,c,args,alias_of aliases)])
+      (match maybe_constructor head intern_pat aliases scopes with
+	 | ConstrPat (c,idspl) ->
+	     check_constructor_length genv loc c idspl [];
+	     let (ids',pll) = product_of_cases_patterns ids idspl in
+	     (ids,List.map (fun (subst,pl) ->
+	       (subst, PatCstr (loc,c,pl,alias_of aliases))) pll)
 	 | VarPat id ->
 	     let ids,subst = merge_aliases aliases id in
 	     (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
@@ -592,8 +692,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       (ids,[subst, PatVar (loc,alias_of aliases)])
   | CPatOr (loc, pl) ->
       assert (pl <> []);
-      let pl' = 
-	List.map (intern_cases_pattern genv scopes aliases tmp_scope) pl in
+      let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
       let (idsl,pl') = List.split pl' in
       let ids = List.hd idsl in
       check_or_pat_variables loc ids (List.tl idsl);
@@ -699,98 +798,13 @@ let extract_explicit_arg imps args =
   in aux args
 
 (**********************************************************************)
-(* Syntax extensions                                                  *)
-
-let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
-  try
-    (* Binders bound in the notation are considered first-order objects *)
-    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    (renaming,(Idset.add id' ids,tmpsc,scopes)), id'
-  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.map snd renaming in
-    let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
-    let id' = next_ident_away id fvs in
-    let renaming' = if id=id' then renaming else (id,id')::renaming in
-    (renaming',env), id'
-
-let decode_constrlist_value = function
-  | CAppExpl (_,_,l) -> l
-  | _ -> anomaly "Ill-formed list argument of notation"
-
-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 (renaming,(ids,_,scopes)) =
-  function
-  | 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,scopt,subscopes@scopes) a
-	with Not_found -> 
-	try 
-	  RVar (loc,List.assoc id renaming)
-	with Not_found -> 
-	  (* Happens for local notation joint with inductive/fixpoint defs *)
-	  RVar (loc,id)
-      end
-  | AList (x,_,iter,terminator,lassoc) ->
-      (try 
-        (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (a,(scopt,subscopes)) = List.assoc x subst in
-        let termin = 
-          subst_aconstr_in_rawconstr loc interp subst 
-	    (renaming,(ids,None,scopes)) terminator in
-        let l = decode_constrlist_value a in
-	List.fold_right (fun a t -> 
-          subst_iterator ldots_var t
-            (subst_aconstr_in_rawconstr loc interp 
-              ((x,(a,(scopt,subscopes)))::subst)
-	      (renaming,(ids,None,scopes)) iter))
-            (if lassoc then List.rev l else l) termin
-      with Not_found -> 
-          anomaly "Inconsistent substitution of recursive notation")
-  | t ->
-      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
-      (subst_aconstr_in_rawconstr loc interp subst)
-      (renaming,(ids,None,scopes)) t
-
-let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
-  let ntn,args = contract_notation ntn args in
-  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-  if !dump then dump_notation_location (ntn_loc loc args ntn) df;
-  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
-  subst_aconstr_in_rawconstr loc intern subst ([],env) c
-
-let set_type_scope (ids,tmp_scope,scopes) =
-  (ids,Some Notation.type_scope,scopes)
-
-let reset_tmp_scope (ids,tmp_scope,scopes) =
-  (ids,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
-
-(**********************************************************************)
 (* Main loop                                                          *)
 
 let internalise sigma globalenv env allow_patvar lvar c =
   let rec intern (ids,tmp_scope,scopes as env) = function
     | CRef ref as x ->
-	let (c,imp,subscopes,l) = intern_reference env lvar ref in
+	let (c,imp,subscopes,l),_ =
+	  intern_applied_reference intern env lvar [] ref in
 	(match intern_impargs c env imp subscopes l with
           | [] -> c
           | l -> RApp (constr_loc x, c, l))
@@ -878,22 +892,24 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
-        let (f,_,args_scopes,_) = intern_reference env lvar ref in
+        let (f,_,args_scopes,_),args =
+	  let args = List.map (fun a -> (a,None)) args in
+	  intern_applied_reference intern env lvar args ref in
 	check_projection isproj (List.length args) f;
-	RApp (loc, f, intern_args env args_scopes args)
+	RApp (loc, f, intern_args env args_scopes (List.map fst args))
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
           (* Compact notations like "t.(f args') args" *)
           | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> isproj,f,args in
-	let (c,impargs,args_scopes,l) =
+	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef ref -> intern_reference env lvar ref
+            | CRef ref -> intern_applied_reference intern env lvar args ref
             | CNotation (loc,ntn,[]) ->
                 let c = intern_notation intern env loc ntn [] in
-                find_appl_head_data lvar c
-            | x -> (intern env f,[],[],[]) in
+                find_appl_head_data lvar c, args
+            | x -> (intern env f,[],[],[]), args in
 	let args = 
 	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
@@ -1296,7 +1312,7 @@ let locate_reference qid =
     | TrueGlobal ref -> ref
     | SyntacticDef kn -> 
 	match Syntax_def.search_syntactic_definition dummy_loc kn with
-	  | Rawterm.RRef (_,ref) -> ref
+	  | [],ARef ref -> ref
 	  | _ -> raise Not_found
 
 let is_global id =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3551746b8..8f42d76c2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -34,7 +34,7 @@ let locate_reference qid =
     | TrueGlobal ref -> ref
     | SyntacticDef kn -> 
 	match Syntax_def.search_syntactic_definition dummy_loc kn with
-	  | Rawterm.RRef (_,ref) -> ref
+	  | [],ARef ref -> ref
 	  | _ -> raise Not_found
 
 let is_global id =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index b81e7e6c8..4c2b7eaef 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -19,7 +19,7 @@ open Nameops
 
 (* Syntactic definitions. *)
 
-let syntax_table = ref (KNmap.empty : aconstr KNmap.t)
+let syntax_table = ref (KNmap.empty : interpretation KNmap.t)
 
 let _ = Summary.declare_summary
 	  "SYNTAXCONSTANT"
@@ -32,28 +32,28 @@ let _ = Summary.declare_summary
 let add_syntax_constant kn c =
   syntax_table := KNmap.add kn c !syntax_table
 
-let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
+  add_syntax_constant kn pat;
   Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
   if not onlyparse then
     (* Declare it to be used as long name *)
-    Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
+    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
-let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) =
+let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
   if not onlyparse then
     (* Redeclare it to be used as (short) name in case an other (distfix)
        notation was declared inbetween *)
-    Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
+    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
 
 let cache_syntax_constant d =
   load_syntax_constant 1 d
 
-let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
-  (local,subst_aconstr subst [] c,onlyparse)
+let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
+  (local,subst_interpretation subst pat,onlyparse)
 
 let classify_syntax_constant (_,(local,_,_ as o)) =
   if local then Dispose else Substitute o
@@ -70,21 +70,18 @@ let (in_syntax_constant, out_syntax_constant) =
     classify_function = classify_syntax_constant;
     export_function = export_syntax_constant } 
 
-let declare_syntactic_definition local id onlyparse c =
-  let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in ()
-
-let rec set_loc loc _ a =
-  rawconstr_of_aconstr_with_binders loc (fun id e -> (id,e)) (set_loc loc) () a
+let declare_syntactic_definition local id onlyparse pat =
+  let _ = add_leaf id (in_syntax_constant (local,pat,onlyparse)) in ()
 
 let search_syntactic_definition loc kn =
-  set_loc loc () (KNmap.find kn !syntax_table)
+  KNmap.find kn !syntax_table
 
 let locate_global_with_alias (loc,qid) =
   match Nametab.extended_locate qid with
   | TrueGlobal ref -> ref
   | SyntacticDef kn -> 
   match search_syntactic_definition dummy_loc kn with
-  | Rawterm.RRef (_,ref) -> ref
+  | [],ARef ref -> ref
   | _ -> 
       user_err_loc (loc,"",pr_qualid qid ++ 
         str " is bound to a notation that does not denote a reference")
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index e83cb8885..bbbea07f3 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,11 +18,10 @@ open Libnames
 
 (* Syntactic definitions. *)
 
-val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
+val declare_syntactic_definition : bool -> identifier -> bool -> interpretation
   -> unit
 
-val search_syntactic_definition : loc -> kernel_name -> rawconstr
-
+val search_syntactic_definition : loc -> kernel_name -> interpretation
 
 (* [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise Not_found
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 05a1465ac..e80065dce 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -361,6 +361,8 @@ let rec subst_aconstr subst bound raw =
 	      if r1' == r1 then raw else
 		ACast (r1',CastCoerce)
 		  
+let subst_interpretation subst (metas,pat) = 
+  (metas,subst_aconstr subst (List.map fst metas) pat)
 
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
@@ -434,7 +436,14 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
   | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
   | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
-  | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+  | RApp (loc,f1,l1), AApp (f2,l2) ->
+      let n1 = List.length l1 and n2 = List.length l2 in
+      let f1,l1,f2,l2 =
+	if n1 < n2 then
+	  let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22
+	else if n1 > n2 then
+	  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 (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) 
       when List.length l1 = List.length l2 ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4e46d9590..3094be0e9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -65,11 +65,6 @@ val rawconstr_of_aconstr_with_binders : loc ->
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
 (**********************************************************************)
-(* Substitution of kernel names, avoiding a list of bound identifiers *)
-
-val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr
-
-(**********************************************************************)
 (* [match_aconstr metas] matches a rawconstr against an aconstr with  *)
 (* metavariables in [metas]; raise [No_match] if the matching fails   *)
 
@@ -86,6 +81,11 @@ val match_aconstr : rawconstr -> interpretation ->
       (rawconstr * (tmp_scope_name option * scope_name list)) list
 
 (**********************************************************************)
+(* Substitution of kernel names in interpretation data                *)
+
+val subst_interpretation : substitution -> interpretation -> interpretation
+
+(**********************************************************************)
 (*s Concrete syntax for terms                                         *)
 
 type notation = string
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index df29d5096..a693ebdb5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -794,9 +794,10 @@ GEXTEND Gram
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (local,(op,modl),p,sc)
-     | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
+     | IDENT "Notation"; local = locality; id = ident; idl = LIST0 ident; 
+	 ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
-           VernacSyntacticDefinition (id,c,local,b)
+           VernacSyntacticDefinition (id,(idl,c),local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 7ca1964ea..a013b4b93 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -816,10 +816,10 @@ let rec pr_vernac = function
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_pattern_expr
-  | VernacSyntacticDefinition (id,c,local,onlyparsing) ->
+  | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
-        (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
-         pr_constrarg c ++
+        (str"Notation " ++ pr_locality local ++ pr_id id ++ 
+	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,e,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 767072e2b..7eb8a538b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -400,11 +400,12 @@ let gallina_print_constant_with_infos sp =
 let gallina_print_syntactic_def kn =
   let sep = " := "
   and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
-  and c = Syntax_def.search_syntactic_definition dummy_loc kn in 
-  str "Notation " ++ pr_qualid qid ++ str sep ++ 
+  and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in 
+  let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
+  str "Notation " ++ pr_qualid qid ++ 
+  prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
   Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
 
-
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
   and tag = object_tag lobj in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4f26cd1eb..fbba7a4ee 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -163,9 +163,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
         declare_global_definition ident ce' local imps in
   hook local r
 
-let syntax_definition ident c local onlyparse =
-  let c = snd (interp_aconstr [] [] c) in
-  Syntax_def.declare_syntactic_definition local ident onlyparse c
+let syntax_definition ident (vars,c) local onlyparse =
+  let pat = interp_aconstr [] vars c in
+  Syntax_def.declare_syntactic_definition local ident onlyparse pat
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 31420d189..942fd2c31 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -39,7 +39,8 @@ val declare_definition : identifier -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> declaration_hook -> unit
 
-val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
+val syntax_definition : identifier -> identifier list * constr_expr -> 
+  bool -> bool -> unit
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
   Impargs.manual_explicitation list -> bool -> Names.variable located  -> unit
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d9a82a413..f8f8c9ad2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -854,8 +854,8 @@ let cache_notation o =
   load_notation 1 o;
   open_notation 1 o
 
-let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) =
-  (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf)
+let subst_notation (_,subst,(lc,scope,pat,b,ndf)) =
+  (lc,scope,subst_interpretation subst pat,b,ndf)
 
 let classify_notation (_,(local,_,_,_,_ as o)) =
   if local then Dispose else Substitute o
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 4579d43a6..839f3ee46 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -287,8 +287,8 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       rec_flag * (lident * bool * raw_tactic_expr) list
   | VernacHints of locality_flag * lstring list * hints
-  | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
-      onlyparsing_flag
+  | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
+      locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * lreference * bool *
       (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr