Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

40 files changed, 258 insertions, 199 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 6baff5da..8bc7ad02 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: argextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Genarg
 open Q_util
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 67492e3e..943a9487 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: egrammar.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -66,41 +66,52 @@ type grammar_constr_prod_item =
 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
   | [] ->
-      Gramext.action (fun loc -> f loc fullenv)
+      Gramext.action (fun loc -> f loc fullsubst)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
-      Gramext.action (fun _ -> make fullenv tl)
+      Gramext.action (fun _ -> make fullsubst tl)
   | GramConstrNonTerminal (typ, Some _) :: tl ->
       (* parse a binding non-terminal *)
-    (match typ with
-    | (ETConstr _| ETOther _) ->
-        Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
-    | ETReference ->
-        Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
-    | ETName ->
-        Gramext.action (fun (na:name located) ->
-	  make (constr_expr_of_name na :: env, envlist) tl)
-    | ETBigint ->
-        Gramext.action (fun (v:Bigint.bigint) ->
-	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
-    | ETConstrList (_,n) ->
-	Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+     (match typ with
+     | (ETConstr _| ETOther _) ->
+	Gramext.action (fun (v:constr_expr) ->
+	  make (v :: constrs, constrlists, binders) tl)
+     | ETReference ->
+        Gramext.action (fun (v:reference) ->
+	  make (CRef v :: constrs, constrlists, binders) tl)
+     | ETName ->
+         Gramext.action (fun (na:name located) ->
+	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
+     | ETBigint ->
+         Gramext.action (fun (v:Bigint.bigint) ->
+	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
+     | ETConstrList (_,n) ->
+	Gramext.action (fun (v:constr_expr list) ->
+	  make (constrs, v::constrlists, binders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gramext.action (fun (v:local_binder list) ->
+	  make (constrs, constrlists, v::binders) tl)
+    | ETBinderList (false,_) ->
+	Gramext.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
   | [] ->
       Gramext.action (fun loc -> f loc fullenv)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
@@ -123,7 +134,7 @@ let make_cases_pattern_action
     | ETConstrList (_,_) ->
         Gramext.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 *)
@@ -271,7 +282,10 @@ type notation_grammar =
     int * Gramext.g_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))
@@ -280,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 decc263d..f6b9f6ad 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: egrammar.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -48,7 +48,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))
@@ -64,5 +69,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 5e79cbd5..92ca4dd1 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extend.ml 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 open Util
 
@@ -45,16 +45,18 @@ 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) * Token.pattern list
+  | ETBinderList of bool * Token.pattern 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 5e79cbd5..ad371872 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 open Util
 
@@ -45,10 +45,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) * Token.pattern list
+  | ETBinderList of bool * Token.pattern list
 
 (* Entries level (left-hand-side of grammar rules) *)
 type constr_entry_key =
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index e56c2e12..e12e2593 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extrawit.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Genarg
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 02b71ddc..1a1b6fe4 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extrawit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Genarg
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bba3d0d6..76b761b1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_constr.ml4 13359 2010-07-30 08:46:55Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -34,11 +34,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_let = 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,
@@ -88,8 +83,8 @@ let lpar_id_coloneq =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
-let impl_ident =
-  Gram.Entry.of_parser "impl_ident"
+let impl_ident_head =
+  Gram.Entry.of_parser "impl_ident_head"
     (fun strm ->
       match Stream.npeek 1 strm with
 	| [(_,"{")] ->
@@ -126,13 +121,13 @@ let ident_with =
           | _ -> raise Stream.Failure)
       | _ -> raise Stream.Failure)
 
-let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
+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
-  binder binder_let binders_let record_declaration
-  binders_let_fixannot typeclass_constraint pattern appl_arg;
+  closed_binder open_binders binder binders binders_fixannot
+  record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -204,7 +199,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"; "}" ->
@@ -214,14 +209,10 @@ GEXTEND Gram
       ] ]
   ;
   forall:
-    [ [ "forall" -> ()
-    | IDENT "Π" -> ()
-    ] ]
+    [ [ "forall" -> () ] ]
   ;
   lambda:
-    [ [ "fun" -> ()
-    | IDENT "λ" -> ()
-    ] ]
+    [ [ "fun" -> () ] ]
   ;
   record_declaration:
     [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
@@ -234,13 +225,13 @@ GEXTEND Gram
       (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
-    [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+    [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c
-      | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
+      | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
           mkCLambdaN loc bl c
-      | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
+      | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = loc_of_binder_let 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
@@ -253,7 +244,7 @@ GEXTEND Gram
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
-          CLetTuple (loc,List.map snd lb,po,c1,c2)
+          CLetTuple (loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
 	    CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
@@ -298,7 +289,7 @@ GEXTEND Gram
       | "cofix" -> false ] ]
   ;
   fix_decl:
-    [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
+    [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
         c=operconstr LEVEL "200" ->
           (id,fst bl,snd bl,c,ty) ] ]
   ;
@@ -310,14 +301,14 @@ GEXTEND Gram
     [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
   ;
   pred_pattern:
-    [ [ ona = OPT ["as"; id=name -> snd id];
+    [ [ ona = OPT ["as"; id=name -> id];
         ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ]
   ;
   case_type:
     [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
   ;
   return_type:
-    [ [ a = OPT [ na = OPT["as"; id=name -> snd id];
+    [ [ a = OPT [ na = OPT["as"; na=name -> na];
                   ty = case_type -> (na,ty) ] ->
         match a with
           | None -> None, None
@@ -365,15 +356,7 @@ GEXTEND Gram
       | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
       | s = string -> CPatPrim (loc, String s) ] ]
   ;
-  binder_list:
-    [ [ idl=LIST1 name; bl=binders_let ->
-      LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
-    | idl=LIST1 name; ":"; c=lconstr ->
-        [LocalRawAssum (idl,Default Explicit,c)]
-    | cl = binders_let -> cl
-    ] ]
-  ;
-  binder_assum:
+  impl_ident_tail:
     [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
     | idl=LIST1 name; ":"; c=lconstr; "}" ->
         (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
@@ -390,47 +373,59 @@ GEXTEND Gram
 	rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
     ] ]
   ;
-  binders_let_fixannot:
-    [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
-	(assum (loc, Name id) :: fst bl), snd bl
-    | f = fixannot -> [], f
-    | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
-    | -> [], (None, CStructRec)
+  binders_fixannot:
+    [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot ->
+          (assum (loc, Name id) :: fst bl), snd bl
+      | f = fixannot -> [], f
+      | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
+      | -> [], (None, CStructRec)
     ] ]
   ;
-  binders_let:
-    [ [ b = binder_let; bl = binders_let -> b @ bl
-    | -> [] ] ]
-  ;
-  binder_let:
-    [ [ id=name ->
-      [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
-    | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
-        [LocalRawAssum (id::idl,Default Explicit,c)]
-    | "("; id=name; ":"; c=lconstr; ")" ->
-        [LocalRawAssum ([id],Default Explicit,c)]
-    | "("; id=name; ":="; c=lconstr; ")" ->
-        [LocalRawDef (id,c)]
-    | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-        [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
-    | "{"; id=name; "}" ->
-        [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
-    | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
-        [LocalRawAssum (id::idl,Default Implicit,c)]
-    | "{"; id=name; ":"; c=lconstr; "}" ->
-        [LocalRawAssum ([id],Default Implicit,c)]
-    | "{"; id=name; idl=LIST1 name; "}" ->
-        List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
-    | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
-    | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+  open_binders:
+    (* Same as binders but parentheses around a closed binder are optional if
+       the latter is unique *)
+    [ [ (* open binder *)
+        id = name; idl = LIST0 name; ":"; c = lconstr ->
+          [LocalRawAssum (id::idl,Default Explicit,c)]
+	(* binders factorized with open binder *)
+      | 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'
     ] ]
   ;
+  binders:
+    [ [ l = LIST0 binder -> List.flatten l ] ]
+  ;
   binder:
-    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
-      | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
+    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+      | bl = closed_binder -> bl ] ]
+  ;
+  closed_binder:
+    [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+          [LocalRawAssum (id::idl,Default Explicit,c)]
+      | "("; id=name; ":"; c=lconstr; ")" ->
+          [LocalRawAssum ([id],Default Explicit,c)]
+      | "("; id=name; ":="; c=lconstr; ")" ->
+          [LocalRawDef (id,c)]
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+      | "{"; id=name; "}" ->
+          [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+          [LocalRawAssum (id::idl,Default Implicit,c)]
+      | "{"; id=name; ":"; c=lconstr; "}" ->
+          [LocalRawAssum ([id],Default Implicit,c)]
+      | "{"; id=name; idl=LIST1 name; "}" ->
+          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+      | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+      | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index c9da8779..0aa8272b 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_decl_mode.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 
 open Decl_expr
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index d5c8b78b..e0f31b98 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_ltac.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
index 5ad93c9e..21335332 100644
--- a/parsing/g_natsyntax.mli
+++ b/parsing/g_natsyntax.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: g_natsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Nice syntax for naturals. *)
 
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 5c2fadbb..a7ed810d 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(*i $Id$ i*)
+(*i $Id: g_prim.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pcoq
 open Names
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 779e4b22..df23465e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_proofs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 
 open Pcoq
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 324119ed..4a1b9c63 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_tactic.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Pcoq
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c3ea4d22..1f5a6cf9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 
 open Pp
@@ -134,9 +134,9 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+    [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
         l = LIST0
-          [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+          [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
             (Some id,(bl,c,None)) ] ->
           VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list ->
@@ -170,7 +170,7 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
-        ps = binders_let;
+        ps = binders;
 	s = OPT [ ":"; s = lconstr -> s ];
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
@@ -231,13 +231,13 @@ GEXTEND Gram
   ;
   (* Simple definitions *)
   def_body:
-    [ [ bl = binders_let; ":="; red = reduce; c = lconstr ->
+    [ [ bl = binders; ":="; red = reduce; c = lconstr ->
       (match c with
           CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
-    | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+    | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
 	DefineBody (bl, red, c, Some t)
-    | bl = binders_let; ":"; t = lconstr ->
+    | bl = binders; ":"; t = lconstr ->
         ProveBody (bl, t) ] ]
   ;
   reduce:
@@ -254,7 +254,7 @@ GEXTEND Gram
   ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; oc = opt_coercion; indpar = binders_let;
+    [ [ id = identref; oc = opt_coercion; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
@@ -281,13 +281,13 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = identref;
-	bl = binders_let_fixannot;
+	bl = binders_fixannot;
         ty = type_cstr;
 	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
 	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = identref; bl = binders_let; ty = type_cstr; 
+    [ [ id = identref; bl = binders; ty = type_cstr;
         def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -305,6 +305,10 @@ GEXTEND Gram
           IDENT "Sort"; s = sort-> InductionScheme(true,ind,s)
       | IDENT "Minimality"; "for"; ind = smart_global;
           IDENT "Sort"; s = sort-> InductionScheme(false,ind,s)
+      | IDENT "Elimination"; "for"; ind = smart_global;
+          IDENT "Sort"; s = sort-> CaseScheme(true,ind,s)
+      | IDENT "Case"; "for"; ind = smart_global;
+          IDENT "Sort"; s = sort-> CaseScheme(false,ind,s)
       | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ]
   ;
   (* Various Binders *)
@@ -324,12 +328,12 @@ GEXTEND Gram
     [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
   ;
   record_binder_body:
-    [ [ l = binders_let; oc = of_type_with_opt_coercion;
+    [ [ l = binders; oc = of_type_with_opt_coercion;
          t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t))
-      | l = binders_let; oc = of_type_with_opt_coercion;
+      | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> fun id ->
 	   (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
-      | l = binders_let; ":="; b = lconstr -> fun id ->
+      | l = binders; ":="; b = lconstr -> fun id ->
          match b with
 	 | CCast(_,b, Rawterm.CastConv (_, t)) ->
 	     (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
@@ -352,7 +356,7 @@ GEXTEND Gram
   ;
 
   constructor_type:
-    [[ l = binders_let;
+    [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (coe,(id,mkCProdN loc l c))
             |  ->
@@ -527,7 +531,7 @@ GEXTEND Gram
          t = class_rawexpr ->
 	  VernacCoercion (use_locality_exp (), ByNotation ntn, s, t)
 
-      | IDENT "Context"; c = binders_let ->
+      | IDENT "Context"; c = binders ->
 	  VernacContext c
 
       | IDENT "Instance"; namesup = instance_name; ":";
@@ -577,7 +581,7 @@ GEXTEND Gram
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
   instance_name:
-    [ [ name = identref; sup = OPT binders_let ->
+    [ [ name = identref; sup = OPT binders ->
 	  (let (loc,id) = name in (loc, Name id)),
           (Option.default [] sup)
       | -> (loc, Anonymous), []  ] ]
@@ -922,6 +926,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/g_xml.ml4 b/parsing/g_xml.ml4
index b75d55c5..5ad9f664 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id$ *)
+(* $Id: g_xml.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
index 74637969..16b1ba65 100644
--- a/parsing/g_zsyntax.mli
+++ b/parsing/g_zsyntax.mli
@@ -6,6 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: g_zsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Nice syntax for integers. *)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 59b1a048..cc48c84f 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -10,7 +10,7 @@
 (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
  * ast-based camlp4 *)
 
-(*i $Id$ i*)
+(*i $Id: lexer.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 35836f5c..a25774c5 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: lexer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6a85775d..90a9220f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
-(*i $Id$ i*)
+(*i $Id: pcoq.ml4 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 open Pp
 open Util
@@ -313,10 +313,11 @@ module Constr =
     let pattern = Gram.Entry.create "constr:pattern"
     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 binder_let = Gram.Entry.create "constr:binder_let"
-    let binders_let = Gram.Entry.create "constr:binders_let"
-    let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
+    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"
     let appl_arg = Gram.Entry.create "constr:appl_arg"
@@ -563,10 +564,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 =
@@ -606,6 +612,12 @@ let is_binder_level from e =
       ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true
     | _ -> false
 
+let make_sep_rules tkl =
+  Gramext.srules
+    [List.map (fun x -> Gramext.Stoken x) tkl,
+     List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
+       (Gramext.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
@@ -621,10 +633,14 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
     | ETConstrList (typ',tkl) ->
         Gramext.Slist1sep
           (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
-           Gramext.srules
-             [List.map (fun x -> Gramext.Stoken x) tkl,
-              List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
-                (Gramext.action (fun loc -> ()))])
+	   make_sep_rules tkl)
+    | ETBinderList (false,[]) ->
+        Gramext.Slist1
+	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+    | ETBinderList (false,tkl) ->
+        Gramext.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,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 88bf9c1c..e4566e77 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pcoq.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 open Util
 open Names
@@ -203,10 +203,11 @@ module Constr :
     val pattern : cases_pattern_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
     val lconstr_pattern : constr_expr Gram.Entry.e
-    val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
-    val binder_let : local_binder list Gram.Entry.e
-    val binders_let : local_binder list Gram.Entry.e
-    val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
+    val closed_binder : local_binder list Gram.Entry.e
+    val binder : local_binder list Gram.Entry.e (* closed_binder or variable *)
+    val binders : local_binder list Gram.Entry.e
+    val open_binders : local_binder list Gram.Entry.e
+    val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
     val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
     val record_declaration : constr_expr Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index fcdc2aee..eef28fcf 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: ppconstr.ml 13358 2010-07-29 23:10:17Z herbelin $ *)
 
 (*i*)
 open Util
@@ -64,8 +64,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 ()
@@ -76,6 +76,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 *)
@@ -85,9 +87,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)
@@ -191,7 +193,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
@@ -254,18 +257,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
@@ -399,7 +406,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
 
@@ -446,7 +453,7 @@ let tm_clash = function
 
 let pr_asin pr (na,indnalopt) =
   (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
-    | Some na -> spc () ++ str "as " ++  pr_name na
+    | Some na -> spc () ++ str "as " ++  pr_lname na
     | None -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
@@ -465,7 +472,7 @@ let pr_return_type pr po = pr_case_type pr po
 
 let pr_simple_return_type pr na po =
   (match na with
-    | Some (Name id) ->
+    | Some (_,Name id) ->
         spc () ++ str "as " ++  pr_id id
     | _ -> mt ()) ++
   pr_case_type pr po
@@ -483,15 +490,11 @@ let pr_app pr a l =
     pr (lapp,L) a  ++
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
-let pr_forall () =
-  if !Flags.unicode_syntax then str"Π" ++ spc ()
-  else str"forall" ++ spc ()
+let pr_forall () = str"forall" ++ spc ()
 
-let pr_fun () =
-  if !Flags.unicode_syntax then str"λ" ++ spc ()
-  else str"fun" ++ spc ()
+let pr_fun () = str"fun" ++ spc ()
 
-let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>")
+let pr_fun_sep = str " =>"
 
 
 let pr_dangling_with_for sep pr inherited a =
@@ -519,16 +522,16 @@ 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),
+	       pr_fun_sep ++ pr spc ltop a),
       llambda
   | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
@@ -599,7 +602,7 @@ let pr pr sep inherited a =
       hv 0 (
         str "let " ++
 	hov 0 (str "(" ++
-               prlist_with_sep sep_v pr_name nal ++
+               prlist_with_sep sep_v pr_lname nal ++
                str ")" ++
 	       pr_simple_return_type (pr mt) na po ++ str " :=" ++
                pr spc ltop c ++ str " in") ++
@@ -626,9 +629,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
@@ -700,7 +704,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/ppconstr.mli b/parsing/ppconstr.mli
index 0d566a5d..1ad110cb 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ppconstr.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Environ
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index b276444f..275b02df 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: ppdecl_proof.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ba7558f7..f27959c2 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pptactic.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Names
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 46786997..bb9d8426 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pptactic.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Genarg
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 83fcff7e..ff35be57 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Names
@@ -113,7 +113,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
@@ -330,6 +332,14 @@ let pr_onescheme (idop,schem) =
     hov 0 ((if dep then str"Induction for" else str"Minimality for")
     ++ spc() ++ pr_smart_global ind) ++ spc() ++
     hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
+  | CaseScheme (dep,ind,s) ->
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc ()
+    ) ++
+    hov 0 ((if dep then str"Elimination for" else str"Case for")
+    ++ spc() ++ pr_smart_global ind) ++ spc() ++
+    hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
   | EqualityScheme ind ->
     (match idop with
       | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index f1322914..dce1bbd7 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ppvernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Genarg
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8f12ec6d..9c39e57e 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id$ *)
+(* $Id: prettyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 9cda516e..d7f83b63 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: prettyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 54d7065c..c9f27678 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 63493768..a6f73a40 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 84340cae..fff29083 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: q_constr.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Rawterm
 open Term
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 0f2ef78b..d0afcdd4 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
 
-(* $Id$ *)
+(* $Id: q_coqast.ml4 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 open Util
 open Names
@@ -162,11 +162,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/parsing/q_util.ml4 b/parsing/q_util.ml4
index a23e4b18..6d6c229c 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: q_util.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 7617dc53..c55d8482 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: q_util.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 val patt_of_expr : MLast.expr -> MLast.patt
 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 465465fa..f067fcf3 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Genarg
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index ff87ac03..3d048c30 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tactic_printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 3584f626..9233233f 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tactic_printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 05c5ef86..95eccfda 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id$ *)
+(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Genarg