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

43 files changed, 303 insertions, 208 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 809af337..6064c3d4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: auto_ind_decl.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* This file is about the automatic generation of schemes about
    decidable equality, created by Vincent Siles, Oct 2007 *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 071731ac..5828f12d 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index e2c42d50..00316007 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 49b3399c..0ee9dd19 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: class.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 7410ed32..057d85ac 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: class.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4c334e0b..435ddb4d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -149,7 +149,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
     let (env', ctx), imps = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+    let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index a19d5dbb..61670e0d 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1f6e7e83..9b18ef27 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
 
 open Pp
 open Util
@@ -69,8 +69,7 @@ let red_constant_entry n ce = function
 let interp_definition boxed bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_bl, ctx), imps1 =
-    interp_context_evars ~fail_anonymous:false evdref env bl in
+  let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
   let imps,ce =
     match ctypopt with
       None ->
@@ -227,7 +226,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let env0 = Global.env() in
   let evdref = ref Evd.empty in
   let (env_params, ctx_params), userimpls =
-    interp_context_evars ~fail_anonymous:false evdref env0 paramsl
+    interp_context_evars evdref env0 paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
@@ -244,7 +243,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
   let arities = List.map fst arities in
-  let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in
+  let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
@@ -256,9 +255,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
      () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_params !evdref in
+  let evd = consider_remaining_unif_problems env_params !evdref in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
-  let sigma =  evd in
+  let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
@@ -448,14 +447,19 @@ let check_mutuality env isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
+  fix_annot : identifier located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
 
-let interp_fix_context evdref env fix =
-  interp_context_evars evdref env fix.fix_binders
-
+let interp_fix_context evdref env isfix fix =
+  let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
+  let (env', ctx), imps = interp_context_evars evdref env before in
+  let (env'', ctx'), imps' = interp_context_evars evdref env' after in
+  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
+    ((env'', ctx' @ ctx), imps @ imps', annot)
+      
 let interp_fix_ccl evdref (env,_) fix =
   interp_type_evars evdref env fix.fix_type
 
@@ -487,8 +491,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences na fix (ids,_) =
-  match index_of_annot fix.fix_binders na with
+let compute_possible_guardness_evidences (ids,_,na) =
+  match na with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -507,15 +511,15 @@ let interp_recursive isfix fixl notations =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref Evd.empty in
-  let fixctxs, fiximps =
-    List.split (List.map (interp_fix_context evdref env) fixl) in
+  let fixctxs, fiximps, fixannots =
+    list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in
+  let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
@@ -525,7 +529,7 @@ let interp_recursive isfix fixl notations =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd,_ = consider_remaining_unif_problems env_rec !evdref in
+  let evd = consider_remaining_unif_problems env_rec !evdref in
   let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
   let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
@@ -538,7 +542,7 @@ let interp_recursive isfix fixl notations =
   end;
 
   (* Build the fix declaration block *)
-  (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps
+  (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let interp_fixpoint = interp_recursive true
 let interp_cofixpoint = interp_recursive false
@@ -547,7 +551,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -558,7 +562,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
-    let fiximps = List.map snd fiximps in
+    let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
@@ -572,7 +576,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -583,7 +587,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let fiximps = List.map snd fiximps in
+    let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -592,28 +596,28 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   List.iter Metasyntax.add_notation_interpretation ntns
 
 let extract_decreasing_argument = function
-  | (_,(na,CStructRec),_,_,_) -> na
+  | (na,CStructRec) -> na
   | _ -> error 
       "Only structural decreasing is supported for a non-Program Fixpoint"
 
 let extract_fixpoint_components l =
   let fixl, ntnl = List.split l in
-  let wfl = List.map extract_decreasing_argument fixl in
-  let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
-    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
-  fixl, List.flatten ntnl, wfl
+  let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+    let ann = extract_decreasing_argument ann in
+      {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+  fixl, List.flatten ntnl
 
 let extract_cofixpoint_components l =
   let fixl, ntnl = List.split l in
   List.map (fun ((_,id),bl,typ,def) ->
-    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+    {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
 let do_fixpoint l b =
-  let fixl,ntns,wfl = extract_fixpoint_components l in
+  let fixl,ntns = extract_fixpoint_components l in
   let fix = interp_fixpoint fixl ntns in
   let possible_indexes =
-    list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in
+    List.map compute_possible_guardness_evidences (snd fix) in
   declare_fixpoint b fix possible_indexes ntns
 
 let do_cofixpoint l b =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ab94e7d2..f5996905 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: command.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -102,6 +102,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
+  fix_annot : identifier located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
@@ -112,8 +113,7 @@ type structured_fixpoint_expr = {
 
 val extract_fixpoint_components :
   (fixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list *
-    (* possible structural arg: *) lident option list
+    structured_fixpoint_expr list * decl_notation list
 
 val extract_cofixpoint_components :
   (cofixpoint_expr * decl_notation list) list ->
@@ -126,20 +126,20 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (name list * manual_implicits) list
+    recursive_preentry * (name list * manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (name list * manual_implicits) list
+    recursive_preentry * (name list * manual_implicits * int option) list
 
 (* Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  bool -> recursive_preentry * (name list * manual_implicits) list -> 
+  bool -> recursive_preentry * (name list * manual_implicits * int option) list -> 
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  bool -> recursive_preentry * (name list * manual_implicits) list ->
+  bool -> recursive_preentry * (name list * manual_implicits * int option) list ->
     decl_notation list -> unit
 
 (* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5f9f96a9..bce38128 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: coqinit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open System
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 926ecf8f..c2a535dd 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: coqinit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Initialization. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3d3010dd..f05509a4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: coqtop.ml 13358 2010-07-29 23:10:17Z herbelin $ *)
 
 open Pp
 open Util
@@ -281,7 +281,7 @@ let parse_args is_ide =
     | "-emacs-U" :: rem -> Flags.print_emacs := true;
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
 
-    | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+    | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
 
     | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
     | "-coqlib" :: [] -> usage ()
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index f5e3a464..e80b3252 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: coqtop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index af02253b..6f74c526 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: discharge.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Util
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index a2cbb6be..dda4c5d7 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: discharge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Sign
 open Cooking
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a97bf9bb..a080442c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -543,7 +543,7 @@ let explain_unsatisfiable_constraints env evd constr =
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
-	pr_constraints true env evm
+	pr_constraints true env undef
   | Some (ev, k) ->
       explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
 	if List.length (Evd.to_list undef) > 1 then
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 856583d9..a916e87b 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: himsg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6f692ced..4e28ccac 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* File created by Vincent Siles, Oct 2007, extended into a generic
    support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ef3efa47..29d7a12c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *)
 
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
@@ -54,7 +54,7 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
-let case_flag = ref true
+let case_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -63,7 +63,7 @@ let _ =
       optread  = (fun () -> !case_flag) ;
       optwrite = (fun b -> case_flag := b) }
 
-let eq_flag = ref true
+let eq_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -292,6 +292,7 @@ let rec split_scheme l =
   | (Some id,t)::q -> let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
+      | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
       | EqualityScheme  x -> l1,((Some id,smart_global_inductive x)::l2)
     )
 (*
@@ -299,38 +300,41 @@ let rec split_scheme l =
 requested
 *)
   | (None,t)::q ->
-       let l1,l2 = split_scheme q in
-    ( match t with
-      | InductionScheme (x,y,z) ->
-             let ind = smart_global_inductive y in
-             let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
-             let z' = family_of_sort (interp_sort z) in
-             let suffix = (
-                match sort_of_ind with
-                | InProp ->
-                    if x then (match z' with
-                       | InProp -> "_ind_nodep"
-                       | InSet -> "_rec_nodep"
-                       | InType -> "_rect_nodep")
-                    else ( match z' with
-                       | InProp -> "_ind"
-                       | InSet -> "_rec"
-                       | InType -> "_rect" )
-                | _ ->
-                    if x then (match z' with
-                       | InProp -> "_ind"
-                       | InSet -> "_rec"
-                       | InType -> "_rect" )
-                    else (match z' with
-                       | InProp -> "_ind_dep"
-                       | InSet  -> "_rec_dep"
-                       | InType -> "_rect_dep")
-                ) in
-            let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
-            let newref = (dummy_loc,newid) in
+      let l1,l2 = split_scheme q in
+      let names inds recs x y z =
+        let ind = smart_global_inductive y in
+        let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
+        let z' = family_of_sort (interp_sort z) in
+        let suffix = (
+          match sort_of_ind with
+          | InProp ->
+              if x then (match z' with
+              | InProp -> inds ^ "_nodep"
+              | InSet -> recs ^ "_nodep"
+              | InType -> recs ^ "t_nodep")
+              else ( match z' with
+              | InProp -> inds
+              | InSet -> recs
+              | InType -> recs ^ "t" )
+          | _ ->
+              if x then (match z' with
+              | InProp -> inds
+              | InSet -> recs
+              | InType -> recs ^ "t" )
+              else (match z' with
+              | InProp -> inds ^ "_dep"
+              | InSet  -> recs ^ "_dep"
+              | InType -> recs ^ "t_dep")
+        ) in
+        let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+        let newref = (dummy_loc,newid) in
           ((newref,x,ind,z)::l1),l2
-      | EqualityScheme  x -> l1,((None,smart_global_inductive x)::l2)
-    )
+      in
+	match t with
+	| CaseScheme (x,y,z) -> names "_case" "_case" x y z
+	| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
+	| EqualityScheme  x -> l1,((None,smart_global_inductive x)::l2)
+	    
 
 let do_mutual_induction_scheme lnamedepindsort =
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 76a5e4b7..f763e182 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: indschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 89252e54..7af5d0aa 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: lemmas.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index e0700341..5327f63f 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: lemmas.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a297d1d7..6ee00f48 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 open Pp
 open Flags
@@ -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 ()
@@ -849,13 +917,13 @@ let compute_syntax_data (df,modifiers) =
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.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 +932,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 +1006,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 +1016,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 +1033,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 +1046,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 +1082,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 +1176,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/metasyntax.mli b/toplevel/metasyntax.mli
index 2fd7749d..d8dd0d52 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: metasyntax.mli 13328 2010-07-26 11:05:30Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -47,7 +47,7 @@ val add_notation_interpretation :
 
 (* Add a notation interpretation for supporting the "where" clause *)
 
-val set_notation_for_interpretation : Constrintern.full_internalization_env ->
+val set_notation_for_interpretation : Constrintern.internalization_env ->
   (lstring * constr_expr * scope_name option) -> unit
 
 (* Add only the parsing/printing rule of a notation *)
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 5cefe263..e8c06d13 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
  * camlp4deps will not work for this file unless Makefile system enhanced.
  *)
 
-(* $Id$ *)
+(* $Id: mltop.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index c2d65493..12b6f78f 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mltop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* If there is a toplevel under Coq, it is described by the following
    record. *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ae53b0cf..cd569178 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -32,7 +32,6 @@ open Topconstr
 (********** definition d'un record (structure) **************)
 
 let interp_evars evdref env impls k typ =
-  let impls = set_internalization_env_params impls [] in
   let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
@@ -48,8 +47,7 @@ let interp_fields_evars evars env nots l =
 	| Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
       in
       let d = (i,b',t') in
-      let impls' = set_internalization_env_params impls [] in
-      List.iter (Metasyntax.set_notation_for_interpretation impls') no;
+      List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
     (env, [], [], []) nots l
 
@@ -62,13 +60,13 @@ let binders_of_decls = List.map binder_of_decl
 let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
   let evars = ref Evd.empty in
-  let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
+  let (env1,newps), imps = interp_context_evars evars env0 ps in
   let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar nots (binders_of_decls fs)
   in
-  let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
+  let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
   let evars = Typeclasses.resolve_typeclasses env_ar evars in
   let sigma =  evars in
   let newps = Evarutil.nf_rel_context_evar sigma newps in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index eae279f3..ea4a3b7e 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: record.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/search.ml b/toplevel/search.ml
index a358f687..0bd552af 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/toplevel/search.mli b/toplevel/search.mli
index b4b971a7..a73052f2 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: search.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Names
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 64096152..9594c988 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 92c8ddc4..a614c1da 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: toplevel.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index dcee9921..22588f2c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: usage.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 662f56ad..1167750b 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: usage.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Prints the version number on the standard output and exits (with 0). *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 17792579..7f8bcb9e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (* Parsing of vernacular. *)
 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d925614c..dc4d9e2f 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Parsing of vernacular. *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3a5e1da8..254f690c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -626,7 +626,6 @@ let vernac_instance abst glob sup inst props pri =
   ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
 
 let vernac_context l =
-  List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
   Classes.context l
 
 let vernac_declare_instance glob id =
@@ -1079,7 +1078,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
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 031864fd..10ed35a7 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vernacentries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 1f3261e1..5eb220cb 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
 
 open Util
 open Names
@@ -197,6 +197,7 @@ type proof_end =
 
 type scheme =
   | InductionScheme of bool * reference or_by_notation * sort_expr
+  | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
 type vernac_expr =
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 90d8d9dd..f3d2e7a5 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: vernacinterp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 8bcbe5f3..ce64188c 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vernacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Tacexpr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 20928cbe..15caaddd 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
+(* $Id: whelp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Flags
 open Pp
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index d6beeca1..27c36239 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: whelp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (* Coq interface to the Whelp query engine developed at
    the University of Bologna *)