Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

35 files changed, 439 insertions, 354 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a7241399e0..46be0b8a1f 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,56 +19,57 @@ let loc_of_or_by_notation f = function
   | AN c -> f c
   | ByNotation (loc,s,_) -> loc
 
-let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
-  Obj.magic t
-
-let wit_int_or_var = unsafe_of_type IntOrVarArgType
+let wit_int_or_var =
+  Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
 
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
-  Genarg.make0 None "intropattern"
+  Genarg.make0 "intropattern"
 
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
-  Genarg.make0 None "tactic"
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+  Genarg.make0 "tactic"
 
-let wit_ident = unsafe_of_type IdentArgType
+let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
 
-let wit_var = unsafe_of_type VarArgType
+let wit_ident =
+  Genarg.make0 "ident"
 
-let wit_ref = Genarg.make0 None "ref"
+let wit_var =
+  Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var"
 
-let wit_quant_hyp = unsafe_of_type QuantHypArgType
+let wit_ref = Genarg.make0 "ref"
 
-let wit_genarg = unsafe_of_type GenArgType
+let wit_quant_hyp = Genarg.make0 "quant_hyp"
 
 let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
-  Genarg.make0 None "sort"
+  Genarg.make0 "sort"
 
-let wit_constr = unsafe_of_type ConstrArgType
+let wit_constr =
+  Genarg.make0 "constr"
 
-let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+let wit_constr_may_eval =
+  Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
 
-let wit_uconstr = Genarg.make0 None "uconstr"
+let wit_uconstr = Genarg.make0 "uconstr"
 
-let wit_open_constr = unsafe_of_type OpenConstrArgType
+let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
+let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings"
 
-let wit_bindings = unsafe_of_type BindingsArgType
+let wit_bindings = Genarg.make0 "bindings"
 
 let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
-  Genarg.make0 None "hyp_location_flag"
+  Genarg.make0 "hyp_location_flag"
 
-let wit_red_expr = unsafe_of_type RedExprArgType
+let wit_red_expr = Genarg.make0 "redexpr"
 
 let wit_clause_dft_concl  =
-  Genarg.make0 None "clause_dft_concl"
+  Genarg.make0 "clause_dft_concl"
 
-(** Register location *)
+(** Aliases *)
 
-let () =
-  register_name0 wit_ref "Constrarg.wit_ref";
-  register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
-  register_name0 wit_tactic "Constrarg.wit_tactic";
-  register_name0 wit_sort "Constrarg.wit_sort";
-  register_name0 wit_uconstr "Constrarg.wit_uconstr";
-  register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index fdeddd66a1..d38b1183c5 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 (** {5 Additional generic arguments} *)
 
-val wit_int_or_var : int or_var uniform_genarg_type
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
 val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 
@@ -38,8 +38,6 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
-val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
-
 val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
 
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
@@ -52,17 +50,17 @@ val wit_constr_may_eval :
 val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
-  (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
+  (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
   glob_constr_and_expr with_bindings,
-  constr with_bindings Evd.sigma) genarg_type
+  constr with_bindings delayed_open) genarg_type
 
 val wit_bindings :
   (constr_expr bindings,
   glob_constr_and_expr bindings,
-  constr bindings Evd.sigma) genarg_type
+  constr bindings delayed_open) genarg_type
 
 val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
 
@@ -71,6 +69,23 @@ val wit_red_expr :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
+
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+    toplevel interpretation. The one of [wit_ltac] forces the tactic and
+    discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d07..c5730e6261 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
       eq_reference c1 c2 &&
-      List.equal cases_pattern_expr_eq a1 a2 &&
+      Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
   | CPatAtom(_,r1), CPatAtom(_,r2) ->
       Option.equal eq_reference r1 r2
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
       Option.equal Int.equal proj1 proj2 &&
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
-  | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+  | CRecord (_, l1), CRecord (_, l2) ->
     let field_eq (r1, e1) (r2, e2) =
       eq_reference r1 r2 && constr_expr_eq e1 e2
     in
-    Option.equal constr_expr_eq e1 e2 &&
     List.equal field_eq l1 l2
   | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
       (** Don't care about the case_style *)
@@ -178,7 +177,7 @@ and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
   Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
@@ -238,7 +237,7 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
-  | CRecord (loc,_,_) -> loc
+  | CRecord (loc,_) -> loc
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 10c84b8dd6..3f5be48559 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb0..592f593330 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,6 +29,8 @@ open Notation
 open Detyping
 open Misctypes
 open Decl_kinds
+
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (* Translation from glob_constr to front constr *)
@@ -147,8 +149,17 @@ let extern_evar loc n l = CEvar (loc,n,l)
     For instance, in the debugger the tables of global references
     may be inaccurate *)
 
+let safe_shortest_qualid_of_global vars r =
+  try shortest_qualid_of_global vars r
+  with Not_found ->
+    match r with
+    | VarRef v -> make_qualid DirPath.empty v
+    | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
+    | IndRef (i,_) | ConstructRef ((i,_),_) ->
+        make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
+
 let default_extern_reference loc vars r =
-  Qualid (loc,shortest_qualid_of_global vars r)
+  Qualid (loc,safe_shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
@@ -255,7 +266,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args =
 
 let mkPat loc qid l =
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
-  if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
+  if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -275,7 +286,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+      CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
     | _ ->
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -316,15 +327,15 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
-		  if !Topconstr.oldfashion_patterns then
+		  if !Topconstr.asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
-		    then CPatCstr (loc, c, [], args)
-		    else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+		    then CPatCstr (loc, c, None, args)
+		    else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
-		      |Some true_args -> CPatCstr (loc, c, [], true_args)
-		      |None -> CPatCstr (loc, c, full_args, [])
+		      |Some true_args -> CPatCstr (loc, c, None, true_args)
+		      |None -> CPatCstr (loc, c, Some full_args, [])
 	  in insert_pat_alias loc p na
 and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
@@ -347,7 +358,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
 		List.map (extern_cases_pattern_in_scope subscope vars) c)
 		substlist in
 	    let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-	    let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2
+	    let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2
 	      else
 		match drop_implicits_in_patt gr nb_to_drop l2 with
 		  |Some true_args -> true_args
@@ -363,7 +374,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
           extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
           subst in
       let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-      let l2' = if !Topconstr.oldfashion_patterns then l2
+      let l2' = if !Topconstr.asymmetric_patterns then l2
 	else
 	  match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
 	    |Some true_args -> true_args
@@ -402,7 +413,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
     let c = extern_reference Loc.ghost vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-    CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
+    CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -420,8 +431,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       let c = extern_reference Loc.ghost vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
-	   |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args)
-	   |None -> CPatCstr (Loc.ghost, c, args, [])
+	   |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
+	   |None -> CPatCstr (Loc.ghost, c, Some args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
@@ -438,8 +449,8 @@ let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
        let n = Recordops.find_projection_nparams r + 1 in
-	 if n <= nargs then None
-	 else Some n
+	 if n <= nargs then Some n
+	 else None
      with Not_found -> None)
   | _ -> None
 	
@@ -453,15 +464,6 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
-let params_implicit n impl = 
-  let rec aux n impl =
-    if n == 0 then true
-    else match impl with
-    | [] -> false
-    | imp :: impl when is_status_implicit imp -> aux (pred n) impl
-    | _ -> false
-  in aux n impl
-
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let explicitize loc inctx impl (cf,f) args =
@@ -680,7 +682,7 @@ let rec extern inctx scopes vars r =
 				 | head :: tail -> ip q locs' tail
 				     ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
-		 CRecord (loc, None, List.rev (ip projs locals args []))
+		 CRecord (loc, List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
 		     extern_app loc inctx
@@ -712,26 +714,29 @@ let rec extern inctx scopes vars r =
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
-      let na' = match na,tm with
-        | Anonymous, GVar (_, id) ->
-            begin match rtntypopt with
-            | None -> None
-            | Some ntn ->
-              if occur_glob_constr id ntn then
-                Some (Loc.ghost, Anonymous)
-              else None
-            end
-        | Anonymous, _ -> None
-        | Name id, GVar (_,id') when Id.equal id id' -> None
-        | Name _, _ -> Some (Loc.ghost,na) in
-      (sub_extern false scopes vars tm,
-       (na',Option.map (fun (loc,ind,nal) ->
-	 let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
-	 let fullargs =
-	   if !Flags.in_debugger then args else
-	     Notation_ops.add_patterns_for_params ind args in
-	 extern_ind_pattern_in_scope scopes vars ind fullargs
-	) x))) tml in
+                 let na' = match na,tm with
+                   | Anonymous, GVar (_, id) ->
+                      begin match rtntypopt with
+                            | None -> None
+                            | Some ntn ->
+                               if occur_glob_constr id ntn then
+                                 Some (Loc.ghost, Anonymous)
+                               else None
+                      end
+                   | Anonymous, _ -> None
+                   | Name id, GVar (_,id') when Id.equal id id' -> None
+                   | Name _, _ -> Some (Loc.ghost,na) in
+                 (sub_extern false scopes vars tm,
+                  na',
+                  Option.map (fun (loc,ind,nal) ->
+                              let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+                              let fullargs =
+                                if !Flags.in_debugger then args else
+                                  Notation_ops.add_patterns_for_params ind args in
+                              extern_ind_pattern_in_scope scopes vars ind fullargs
+                             ) x))
+                tml
+    in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
     CCases (loc,sty,rtntypopt',tml,eqns)
 
@@ -788,7 +793,7 @@ let rec extern inctx scopes vars r =
 	     Miscops.map_cast_type (extern_typ scopes vars) c')
 
 and extern_typ (_,scopes) =
-  extern true (Some Notation.type_scope,scopes)
+  extern true (Notation.current_type_scope_name (),scopes)
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
@@ -977,9 +982,12 @@ let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
   | PEvar (evk,l) ->
-      let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
+      let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
-      let id = Evd.evar_ident evk sigma in
+      let id = match Evd.evar_ident evk sigma with
+      | None -> Id.of_string "__"
+      | Some id -> id
+      in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b797e455c0..f617faa38a 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Termops
 open Environ
 open Libnames
@@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  rel_context -> local_binder list
+  Context.Rel.t -> local_binder list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ecaf2b8c13..a5ee4ce2ec 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,6 +29,7 @@ open Nametab
 open Notation
 open Inductiveops
 open Decl_kinds
+open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
@@ -101,7 +102,7 @@ let global_reference id =
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Context.lookup_named id ctx in id)
+    Term.mkVar (let _ = Context.Named.lookup id ctx in id)
   with Not_found ->
     global_reference id
 
@@ -274,7 +275,8 @@ let error_expect_binder_notation_type loc id =
 
 let set_var_scope loc id istermvar env ntnvars =
   try
-    let idscopes,typ = Id.Map.find id ntnvars in
+    let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
+    if istermvar then isonlybinding := false;
     let () = if istermvar then
       (* scopes have no effect on the interpretation of identifiers *)
       begin match !idscopes with
@@ -298,7 +300,7 @@ let set_var_scope loc id istermvar env ntnvars =
     (* Not in a notation *)
     ()
 
-let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
+let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()}
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
@@ -317,7 +319,7 @@ let rec it_mkGLambda loc2 env body =
 let build_impls = function
   |Implicit -> (function
 		  |Name id ->  Some (id, Impargs.Manual, (true,true))
-		  |Anonymous -> anomaly (Pp.str "Anonymous implicit argument"))
+		  |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
   |Explicit -> fun _ -> None
 
 let impls_type_list ?(args = []) =
@@ -449,12 +451,15 @@ let intern_generalization intern env lvar loc bk ak c =
 	| Some AbsPi -> true
         | Some _ -> false
 	| None ->
-          let is_type_scope = match env.tmp_scope with
+          match Notation.current_type_scope_name () with
+          | Some type_scope ->
+              let is_type_scope = match env.tmp_scope with
+              | None -> false
+              | Some sc -> String.equal sc type_scope
+              in
+              is_type_scope ||
+              String.List.mem type_scope env.scopes
           | None -> false
-          | Some sc -> String.equal sc Notation.type_scope
-          in
-          is_type_scope ||
-          String.List.mem Notation.type_scope env.scopes
       in
 	if pi then
 	  (fun (id, loc') acc ->
@@ -628,7 +633,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
 let split_by_type ids =
   List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
     match typ with
-    | NtnTypeConstr -> ((x,scl)::l1,l2,l3)
+    | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3)
     | NtnTypeConstrList -> (l1,(x,scl)::l2,l3)
     | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[])
 
@@ -685,7 +690,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
       str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
-    let _ = Context.lookup_named id namedctx in
+    let _ = Context.Named.lookup id namedctx in
       try
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
@@ -698,19 +703,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
-let proj_impls r impls =
-  let env = Global.env () in
-  let f (x, l) = x, projection_implicits env r l in
-    List.map f impls
-
-let proj_scopes n scopes = 
-  List.skipn_at_least n scopes
-
-let proj_impls_scopes p impls scopes =
-  match p with
-  | Some (r, n) -> proj_impls r impls, proj_scopes n scopes
-  | None -> impls, scopes
-
 let find_appl_head_data c =
   match c with
   | GRef (loc,ref,_) as x -> 
@@ -929,7 +921,7 @@ let chop_params_pattern loc ind args with_letin =
   args
 
 let find_constructor loc add_params ref =
-  let cstr = match ref with
+  let (ind,_ as cstr) = match ref with
   | ConstructRef cstr -> cstr
   | IndRef _ ->
     let error = str "There is an inductive name deep in a \"in\" clause." in
@@ -938,15 +930,15 @@ let find_constructor loc add_params ref =
     let error = str "This reference is not a constructor." in
     user_err_loc (loc, "find_constructor", error)
   in
-  cstr, (function (ind,_ as c) -> match add_params with
-    |Some nb_args ->
+  cstr, match add_params with
+    | Some nb_args ->
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealdecls c)
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
           then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
       List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
-    |None -> []) cstr
+    | None -> []
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id
@@ -1106,20 +1098,21 @@ let drop_notations_pattern looked_for =
     let (loc,qid) = qualid_of_reference re in
     try
       match locate_extended qid with
-      |SynDef sp ->
+      | SynDef sp ->
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
 	| NRef g ->
+          (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	  test_kind top g;
 	  let () = assert (List.is_empty vars) in
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g, [], List.map2 (in_pat_sc env) argscs pats)
-	| NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *)
+	| NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
 	      test_kind top g;
               let () = assert (List.is_empty vars) in
-	      let (argscs,_) = find_remaining_scopes pats [] g in
-	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
+	      Some (g, List.map (in_pat false env) pats, [])
 	| NApp (NRef g,args) ->
+              (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
@@ -1129,7 +1122,7 @@ let drop_notations_pattern looked_for =
 	      let (_,argscs) = find_remaining_scopes pats1 pats2 g in
 	      Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2)
 	| _ -> raise Not_found)
-      |TrueGlobal g ->
+      | TrueGlobal g ->
 	  test_kind top g;
 	  Dumpglob.add_glob loc g;
 	  let (_,argscs) = find_remaining_scopes [] pats g in
@@ -1142,24 +1135,33 @@ let drop_notations_pattern looked_for =
 	sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
       begin match sorted_fields with
 	| None -> RCPatAtom (loc, None)
-	| Some (_, head, pl) ->
+	| Some (n, head, pl) ->
+          let pl =
+            if !asymmetric_patterns then pl else
+            let pars = List.make n (CPatAtom (loc, None)) in
+            List.rev_append pars pl in
 	  match drop_syndef top env head pl with
 	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, head, [], pl) ->
+    | CPatCstr (loc, head, None, pl) ->
       begin
 	match drop_syndef top env head pl with
 	  | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, r, expl_pl, pl) ->
-      let g = try
-		      (locate (snd (qualid_of_reference r)))
-	    with Not_found ->
+     | CPatCstr (loc, r, Some expl_pl, pl) ->
+      let g = try locate (snd (qualid_of_reference r))
+	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
-      let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in
-      RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl)
+      if expl_pl == [] then
+        (* Convention: (@r) deactivates all further implicit arguments and scopes *)
+        RCPatCstr (loc, g, List.map (in_pat false env) pl, [])
+      else
+        (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
+        (* but not scopes in expl_pl *)
+        let (argscs1,_) = find_remaining_scopes expl_pl pl g in
+        RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl @ List.map (in_pat false env) pl, [])
     | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p))
@@ -1211,8 +1213,8 @@ let drop_notations_pattern looked_for =
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
       RCPatCstr (loc, g,
-		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
-		 List.map2 (in_pat_sc env) argscs2 args)
+		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl @
+		 List.map (in_pat false env) args, [])
     | NList (x,_,iter,terminator,lassoc) ->
       if not (List.is_empty args) then user_err_loc
         (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1245,7 +1247,7 @@ let rec intern_pat genv aliases pat =
       let aliases' = merge_aliases aliases id in
       intern_pat genv aliases' p
     | RCPatCstr (loc, head, expl_pl, pl) ->
-      if !oldfashion_patterns then
+      if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
 	let with_letin =
@@ -1382,7 +1384,7 @@ let internalize globalenv env allow_patvar lvar c =
 	       let (env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in
+	       let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, (env',rbl) =
@@ -1488,7 +1490,7 @@ let internalize globalenv env allow_patvar lvar c =
           apply_impargs c env impargs args_scopes 
 	    (merge_impargs l args) loc
 
-    | CRecord (loc, _, fs) ->
+    | CRecord (loc, fs) ->
 	let cargs =
 	  sort_fields true loc fs
 	    (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l)
@@ -1502,7 +1504,7 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern env app
 	end
     | CCases (loc, sty, rtnpo, tms, eqns) ->
-      let as_in_vars = List.fold_left (fun acc (_,(na,inb)) ->
+      let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x)
 	  (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na)
 	  inb) Id.Set.empty tms in
@@ -1538,7 +1540,7 @@ let internalize globalenv env allow_patvar lvar c =
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
-        let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in
+        let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
@@ -1547,7 +1549,7 @@ let internalize globalenv env allow_patvar lvar c =
                    intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
-      let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *)
+      let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
@@ -1624,7 +1626,7 @@ let internalize globalenv env allow_patvar lvar c =
       let rhs' = intern {env with ids = env_ids} rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
-  and intern_case_item env forbidden_names_for_gen (tm,(na,t)) =
+  and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (*the "match" part *)
     let tm' = intern env tm in
     (* the "as" part *)
@@ -1654,14 +1656,14 @@ let internalize globalenv env allow_patvar lvar c =
 	      |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
-	      |(_,Some _,_)::t, l when not with_letin ->
+	      | LocalDef _ :: t, l when not with_letin ->
 		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
 	      |[],[] ->
 		(add_name match_acc na, var_acc)
 	      |_::t,PatVar (loc,x)::tt ->
 		canonize_args t tt forbidden_names
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
-	      |(cano_name,_,ty)::t,c::tt ->
+	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
 		let fresh =
 		  Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in
 		canonize_args t tt (fresh::forbidden_names)
@@ -1756,7 +1758,7 @@ let extract_ids env =
     Id.Set.empty
 
 let scope_of_type_kind = function
-  | IsType -> Some Notation.type_scope
+  | IsType -> Notation.current_type_scope_name ()
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
@@ -1853,7 +1855,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
 let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in
+  let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
   let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
@@ -1862,7 +1864,8 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
-  let vars = Id.Map.map (fun (sc, typ) -> (out_scope !sc, typ)) vl in
+  let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
+    (!isonlybinding, out_scope !sc, typ)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
   vars, a
 
@@ -1903,7 +1906,7 @@ let interp_rawcontext_evars env evdref k bl =
 	      let t' = locate_if_hole (loc_of_glob_constr t) na t in
 	      let t =
                 understand_tcc_evars env evdref ~expected_type:IsType t' in
-	      let d = (na,None,t) in
+	      let d = LocalAssum (na,t) in
 	      let impls =
 		if k == Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
@@ -1913,7 +1916,7 @@ let interp_rawcontext_evars env evdref k bl =
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
 	      let c = understand_judgment_tcc env evdref b in
-	      let d = (na, Some c.uj_val, c.uj_type) in
+	      let d = LocalDef (na, c.uj_val, c.uj_type) in
 		(push_rel d env, d::params, n, impls))
       (env,[],k+1,[]) (List.rev bl)
   in (env, par), impls
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4d2c994679..eea76aa310 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Evd
 open Environ
 open Libnames
@@ -95,7 +94,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list ->
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Main interpretation functions expecting evars to be all resolved *)
+(** Main interpretation functions, using type class inference,
+    expecting evars and pending problems to be all resolved *)
 
 val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
@@ -106,9 +106,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
 
-(** Main interpretation function expecting evars to be all resolved *)
+(** Main interpretation function expecting all postponed problems to
+    be resolved, but possibly leaving evars. *)
 
-val interp_open_constr   : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
@@ -159,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder list ->
-  internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+  internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -176,7 +177,7 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : named_context -> Id.t -> constr
+val construct_reference : Context.Named.t -> Id.t -> constr
 val global_reference : Id.t -> constr
 val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
 
@@ -184,7 +185,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
     guaranteed to have the same domain as the input one. *)
 val interp_notation_constr : ?impls:internalization_env ->
   notation_interp_env -> constr_expr ->
-  (subscopes * notation_var_internalization_type) Id.Map.t *
+  (bool * subscopes * notation_var_internalization_type) Id.Map.t *
   notation_constr
 
 (** Globalization options *)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5ac718e3b0..23bcddaea2 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -87,7 +87,7 @@ let check_required_library d =
 *)
 (* or failing ...*)
       errorlabstrm "Coqlib.check_required_library"
-        (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+        (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 41204a715b..5ba26d8286 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c18ceecaba..44a62ef379 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -139,12 +139,15 @@ let interval loc =
   loc1, loc2-1
 
 let dump_ref loc filepath modpath ident ty =
-  if !glob_output = Feedback then
+  match !glob_output with
+  | Feedback ->
     Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
-  else
+  | NoGlob -> ()
+  | _ when not (Loc.is_ghost loc) ->
     let bl,el = interval loc in
     dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 		  bl el filepath modpath ident ty)
+  | _ -> ()
 
 let dump_reference loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
@@ -245,7 +248,7 @@ let dump_def ty loc secpath id =
 let dump_definition (loc, id) sec s =
   dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
 
-let dump_constraint ((loc, n), _, _) sec ty =
+let dump_constraint (((loc, n),_), _, _) sec ty =
   match n with
     | Names.Name id -> dump_definition (loc, id) sec ty
     | Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 428189bec0..a7c799114b 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 7795946d56..d6bfd347ff 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -37,20 +37,16 @@ module Subst = Register (SubstObj)
 let intern = Intern.obj
 let register_intern0 = Intern.register0
 
-let generic_intern ist v =
-  let unpacker wit v =
-    let (ist, v) = intern wit ist (raw v) in
-    (ist, in_gen (glbwit wit) v)
-  in
-  unpack { unpacker; } v
+let generic_intern ist (GenArg (Rawwit wit, v)) =
+  let (ist, v) = intern wit ist v in
+  (ist, in_gen (glbwit wit) v)
 
 (** Substitution functions *)
 
 let substitute = Subst.obj
 let register_subst0 = Subst.register0
 
-let generic_substitute subs v =
-  let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in
-  unpack { unpacker; } v
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+  in_gen (glbwit wit) (substitute wit subs v)
 
 let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 28f4f530b2..4b244b38d8 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 87f7a6d6e4..751b03a4a8 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,6 +20,7 @@ open Pp
 open Libobject
 open Nameops
 open Misctypes
+open Context.Rel.Declaration
 (*i*)
 
 let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
@@ -196,7 +197,7 @@ let combine_params avoid fn applied needed =
     List.partition
       (function
 	  (t, Some (loc, ExplByName id)) ->
-            let is_id (_, (na, _, _)) = match na with
+            let is_id (_, decl) = match get_name decl with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
             in
@@ -209,22 +210,22 @@ let combine_params avoid fn applied needed =
     (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
     named
   in
-  let is_unset (_, (_, b, _)) = match b with
-  | None -> true
-  | Some _ -> false
+  let is_unset (_, decl) = match decl with
+  | LocalAssum _ -> true
+  | LocalDef _ -> false
   in
   let needed = List.filter is_unset needed in
   let rec aux ids avoid app need =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named ->
+      | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named ->
 	  aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (Name id, _, _)) :: need ->
+      | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need ->
 	  aux (x :: ids) avoid app need
 
-      | _, (Some cl, (_, _, _) as d) :: need ->
+      | _, (Some cl, _ as d) :: need ->
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -239,8 +240,8 @@ let combine_params avoid fn applied needed =
   in aux [] avoid applied needed
 
 let combine_params_freevar =
-  fun avoid (_, (na, _, _)) ->
-    let id' = next_name_away_from na avoid in
+  fun avoid (_, decl) ->
+    let id' = next_name_away_from (get_name decl) avoid in
       (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
 
 let destClassApp cl =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index a3721af660..d0327e5068 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,7 +28,7 @@ val free_vars_of_binders :
   ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
-   order with the location of their first occurence *)
+   order with the location of their first occurrence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
   glob_constr -> (Id.t * Loc.t) list
@@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
   Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a0315267..96b52959a0 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,12 +3,12 @@ Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
-Topconstr
 Ppextend
 Notation
 Dumpglob
 Syntax_def
 Smartlocate
+Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 35e731137f..e5dce5ccf3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 8b6d002e34..1e04ada17b 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/notation.ml b/interp/notation.ml
index d18b804bfd..b8f4f32017 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -65,11 +65,9 @@ let empty_scope = {
 }
 
 let default_scope = "" (* empty name, not available from outside *)
-let type_scope = "type_scope" (* special scope used for interpreting types *)
 
 let init_scope_map () =
-  scope_map := String.Map.add default_scope empty_scope !scope_map;
-  scope_map := String.Map.add type_scope empty_scope !scope_map
+  scope_map := String.Map.add default_scope empty_scope !scope_map
 
 (**********************************************************************)
 (* Operations on scopes *)
@@ -314,7 +312,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
     patl
 
 let mkNumeral n = Numeral n
-let mkString s = String s
+let mkString = function
+| None -> None
+| Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
 let delay dir int loc x = (dir, (fun () -> int loc x))
 
@@ -326,7 +326,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
+    (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
@@ -529,9 +529,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true
 | NtnTypeConstrList, NtnTypeConstrList -> true
 | NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
 
 let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
@@ -556,23 +557,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 (**********************************************************************)
 (* Mapping classes to scopes *)
 
-type scope_class = ScopeRef of global_reference | ScopeSort
+open Classops
 
-let scope_class_compare sc1 sc2 = match sc1, sc2 with
-| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2
-| ScopeRef _, ScopeSort -> -1
-| ScopeSort, ScopeRef _ -> 1
-| ScopeSort, ScopeSort -> 0
+type scope_class = cl_typ
 
-let scope_class_of_reference x = ScopeRef x
+let scope_class_compare : scope_class -> scope_class -> int =
+  cl_typ_ord
 
 let compute_scope_class t =
-  let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in
-  match kind_of_term t' with
-  | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
-  | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p))
-  | Sort _ -> ScopeSort
-  |  _ -> raise Not_found
+  let (cl,_,_) = find_class_type Evd.empty t in
+  cl
 
 module ScopeClassOrd =
 struct
@@ -583,7 +577,7 @@ end
 module ScopeClassMap = Map.Make(ScopeClassOrd)
 
 let initial_scope_class_map : scope_name ScopeClassMap.t =
-  ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+  ScopeClassMap.empty
 
 let scope_class_map = ref initial_scope_class_map
 
@@ -617,8 +611,11 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t)
 let compute_type_scope t =
   find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
 
-let compute_scope_of_global ref =
-  find_scope_class_opt (Some (ScopeRef ref))
+let current_type_scope_name () =
+   find_scope_class_opt (Some CL_SORT)
+
+let scope_class_of_class (x : cl_typ) : scope_class =
+  x
 
 (** Updating a scope list, thanks to a list of argument classes
     and the current Bind Scope base. When some current scope
@@ -650,12 +647,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) =
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_scope_class subst cs = match cs with
-  | ScopeSort -> Some cs
-  | ScopeRef t ->
-      let (t',c) = subst_global subst t in
-      if t == t' then Some cs
-      else try Some (compute_scope_class c) with Not_found -> None
+let subst_scope_class subst cs =
+  try Some (subst_cl_typ subst cs) with Not_found -> None
 
 let subst_arguments_scope (subst,(req,r,scl,cls)) =
   let r' = fst (subst_global subst r) in
@@ -788,9 +781,7 @@ let pr_delimiters_info = function
 let classes_of_scope sc =
   ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map []
 
-let pr_scope_class = function
-  | ScopeSort -> str "Sort"
-  | ScopeRef t -> pr_global_env Id.Set.empty t
+let pr_scope_class = pr_class
 
 let pr_scope_classes sc =
   let l = classes_of_scope sc in
diff --git a/interp/notation.mli b/interp/notation.mli
index 38bd5fc7b8..480979ccc3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *)
 
 type local_scopes = tmp_scope_name option * scope_name list
 
-val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
@@ -153,7 +152,9 @@ val find_arguments_scope : global_reference -> scope_name option list
 
 type scope_class
 
-val scope_class_of_reference : global_reference -> scope_class
+(** Comparison of scope_class *)
+val scope_class_compare : scope_class -> scope_class -> int
+
 val subst_scope_class :
   Mod_subst.substitution -> scope_class -> scope_class option
 
@@ -162,7 +163,11 @@ val declare_ref_arguments_scope : global_reference -> unit
 
 val compute_arguments_scope : Term.types -> scope_name option list
 val compute_type_scope : Term.types -> scope_name option
-val compute_scope_of_global : global_reference -> scope_name option
+
+(** Get the current scope bound to Sortclass, if it exists *)
+val current_type_scope_name : unit -> scope_name option
+
+val scope_class_of_class : Classops.cl_typ -> scope_class
 
 (** Building notation key *)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2762dc0b8d..6561000c47 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -567,6 +567,18 @@ let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
     (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c))
 
+let is_term_meta id metas =
+  try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
+  with Not_found -> false
+
+let is_onlybinding_meta id metas =
+  try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false
+  with Not_found -> false
+
+let is_bindinglist_meta id metas =
+  try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false
+  with Not_found -> false
+
 exception No_match
 
 let rec alpha_var id1 id2 = function
@@ -575,26 +587,67 @@ let rec alpha_var id1 id2 = function
   | _::idl -> alpha_var id1 id2 idl
   | [] -> Id.equal id1 id2
 
-let add_env alp (sigma,sigmalist,sigmabinders) var v =
+let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
   (* Check that no capture of binding variables occur *)
+  (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
+     with an actual term "fun z => ... z ..." when "x" is not bound in the
+     notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then
+     we keep (z,x) in alp, and we have to check that what the [v] which is bound
+     to [var] does not contain z *)
   if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+  (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
+     with an actual term "fun z => ... z ..." when "x" is bound in the
+     notation and the name "x" cannot be changed to "z", e.g. because
+     used at another occurrence, as in "Notation "'lam' y , P & Q" :=
+     ((fun y => P),(fun y => Q))". Then, we keep (z,y) in alpmetas, and we
+     have to check that "fun z => ... z ..." denotes the same term as
+     "fun x => ... x ... ?var ... x" up to alpha-conversion when [var]
+     is instantiated by [v];
+     Currently, we fail, but, eventually, [x] in [v] could be replaced by [x],
+     and, in match_, when finding "x" in subterm, failing because of a capture,
+     and, in match_, when finding "z" in subterm, replacing it with "x",
+     and, in an even further step, being even more robust, independent of the order, so
+     that e.g. the notation for ex2 works on "x y |- ex2 (fun x => y=x) (fun y => x=y)"
+     by giving, say, "exists2 x0, y=x0 & x=x0", but this would typically require the
+     glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the
+     choice of exact variable be done there; but again, this would be a non-trivial
+     refinement *)
+  if alpmetas != [] then raise No_match;
+  (* TODO: handle the case of multiple occs in different scopes *)
+  ((var,v)::terms,onlybinders,termlists,binderlists)
+
+let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
   (* TODO: handle the case of multiple occs in different scopes *)
-  ((var,v)::sigma,sigmalist,sigmabinders)
+  (terms,(var,v)::onlybinders,termlists,binderlists)
 
-let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
+let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
+  (terms,onlybinders,termlists,(x,List.rev bl)::binderlists)
+
+let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
-    let v' = Id.List.assoc var sigma in
+    let v' = Id.List.assoc var terms in
     match v, v' with
-    | GHole _, _ -> fullsigma
+    | GHole _, _ -> sigma
     | _, GHole _ ->
-      add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v
+        let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
+        add_env alp sigma var v
     | _, _ ->
-        if glob_constr_eq v v' then fullsigma
+        if glob_constr_eq v v' then sigma
         else raise No_match
-  with Not_found -> add_env alp fullsigma var v
+  with Not_found -> add_env alp sigma var v
 
-let bind_binder (sigma,sigmalist,sigmabinders) x bl =
-  (sigma,sigmalist,(x,List.rev bl)::sigmabinders)
+let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+  try
+    let v' = Id.List.assoc var onlybinders in
+    match v, v' with
+    | Anonymous, _ -> alp, sigma
+    | _, Anonymous ->
+        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+        alp, add_binding_env alp sigma var v
+    | Name id1, Name id2 ->
+        if Id.equal id1 id2 then alp,sigma
+        else (fst alp,(id1,id2)::snd alp),sigma
+  with Not_found -> alp, add_binding_env alp sigma var v
 
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
@@ -615,12 +668,16 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (_,Name id2) when Id.List.mem id2 (fst metas) ->
-      let rhs = match na1 with
-      | Name id1 -> GVar (Loc.ghost,id1)
-      | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
-      alp, bind_env alp sigma id2 rhs
-  | (Name id1,Name id2) -> (id1,id2)::alp,sigma
+  | (na1,Name id2) when is_onlybinding_meta id2 metas ->
+      bind_binding_env alp sigma id2 na1
+  | (Name id1,Name id2) when is_term_meta id2 metas ->
+      (* We let the non-binding occurrence define the rhs and hence reason up to *)
+      (* alpha-conversion for the given occurrence of the name (see #)) *)
+      (fst alp,(id1,id2)::snd alp), sigma
+  | (Anonymous,Name id2) when is_term_meta id2 metas ->
+      (* We let the non-binding occurrence define the rhs *)
+      alp, sigma
+  | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
@@ -645,36 +702,38 @@ let rec match_iterated_binders islambda decls = function
 	((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
   | b -> (decls,b)
 
-let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
-  (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders)
+let remove_sigma x (terms,onlybinders,termlists,binderlists) =
+  (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
+
+let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
 let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
   let rec aux sigma acc rest =
     try
-      let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
-      let rest = Id.List.assoc ldots_var (pi1 sigma) in
+      let (terms,_,_,binderlists as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let rest = Id.List.assoc ldots_var terms in
       let b =
-        match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false
+        match Id.List.assoc x binderlists with [b] -> b | _ ->assert false
       in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
       aux sigma (b::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
   let bl,sigma = aux sigma [] rest in
-  bind_binder sigma x bl
+  add_bindinglist_env sigma x bl
 
 let match_alist match_fun metas sigma rest x iter termin lassoc =
   let rec aux sigma acc rest =
     try
-      let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
-      let rest = Id.List.assoc ldots_var (pi1 sigma) in
-      let t = Id.List.assoc x (pi1 sigma) in
+      let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let rest = Id.List.assoc ldots_var terms in
+      let t = Id.List.assoc x terms in
       let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
-  let l,sigma = aux sigma [] rest in
-  (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
+  let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+  (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
 
 let does_not_come_from_already_eta_expanded_var =
   (* This is hack to avoid looping on a rule with rhs of the form *)
@@ -688,11 +747,11 @@ let does_not_come_from_already_eta_expanded_var =
   (* checked). *)
   function GVar _ -> false | _ -> true
 
-let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
+let rec match_ inner u alp metas sigma a1 a2 =
   match (a1,a2) with
 
   (* Matching notation variable *)
-  | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1
+  | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
   | r1, NList (x,_,iter,termin,lassoc) ->
@@ -702,25 +761,26 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
       let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
-      match_in u alp metas (bind_binder sigma x decls) b termin
+      match_in u alp metas (add_bindinglist_env sigma x decls) b termin
   | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
       when na1 != Anonymous ->
       let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
-      match_in u alp metas (bind_binder sigma x decls) b termin
+      match_in u alp metas (add_bindinglist_env sigma x decls) b termin
   (* Matching recursive notations for binders: general case *)
   | r, NBinderList (x,_,iter,termin) ->
       match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas ->
-      match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
+      when is_bindinglist_meta id metas ->
+      match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2
   | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
-      when Id.List.mem id blmetas && na != Anonymous ->
-      match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+      when is_bindinglist_meta id metas && na != Anonymous ->
+      match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2
 
   (* Matching compositionally *)
-  | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
+  | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
   | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
   | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma
   | GApp (loc,f1,l1), NApp (f2,l2) ->
@@ -799,9 +859,9 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
       | NHole _ -> sigma
-      | NVar id2 -> bind_env alp sigma id2 t1
+      | NVar id2 -> bind_term_env alp sigma id2 t1
       | _ -> assert false in
-      match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,t1)])
+      match_in u alp metas (add_bindinglist_env sigma id [(Name id',Explicit,None,t1)])
        (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
 
   | (GRec _ | GEvar _), _
@@ -823,14 +883,16 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
+let term_of_binder = function
+  | Name id -> GVar (Loc.ghost,id)
+  | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+
 let match_notation_constr u c (metas,pat) =
-  let test (_, (_, x)) = match x with NtnTypeBinderList -> false | _ -> true in
-  let vars = List.partition test metas in
-  let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
-  let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
+  let terms,binders,termlists,binderlists =
+    match_ false u ([],[]) metas ([],[],[],[]) c pat in
   (* Reorder canonically the substitution *)
-  let find x =
-    try Id.List.assoc x terms
+  let find_binder x =
+    try term_of_binder (Id.List.assoc x binders)
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
@@ -838,11 +900,13 @@ let match_notation_constr u c (metas,pat) =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
     match typ with
     | NtnTypeConstr ->
-       ((find x, scl)::terms',termlists',binders')
+       ((Id.List.assoc x terms, scl)::terms',termlists',binders')
+    | NtnTypeOnlyBinder ->
+       ((find_binder x, scl)::terms',termlists',binders')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders')
     | NtnTypeBinderList ->
-       (terms',termlists',(Id.List.assoc x binders,scl)::binders'))
+       (terms',termlists',(Id.List.assoc x binderlists,scl)::binders'))
     metas ([],[],[])
 
 (* Matching cases pattern *)
@@ -851,17 +915,17 @@ let add_patterns_for_params ind l =
   let nparams = mib.Declarations.mind_nparams in
     Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
 
-let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
+let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
   try
-    let vvar = Id.List.assoc var sigma in
-    if cases_pattern_eq v vvar then fullsigma else raise No_match
+    let vvar = Id.List.assoc var terms in
+    if cases_pattern_eq v vvar then sigma else raise No_match
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
-    (var,v)::sigma,sigmalist,x
+    (var,v)::terms,x,termlists,y
 
-let rec match_cases_pattern metas sigma a1 a2 =
+let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
  match (a1,a2) with
-  | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
   | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
   | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
       sigma,(0,add_patterns_for_params (fst r1) largs)
@@ -876,14 +940,14 @@ let rec match_cases_pattern metas sigma a1 a2 =
 	let l1',more_args = Util.List.chop le2 l1 in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   | r1, NList (x,_,iter,termin,lassoc) ->
-      (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
-	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[])
+      (match_alist (match_cases_pattern_no_more_args)
+	metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      |out,(_,[]) -> out
-      |_ -> raise No_match
+      | out,(_,[]) -> out
+      | _ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
@@ -904,16 +968,15 @@ let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
       | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
+      | NtnTypeOnlyBinder -> assert false
       | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
       | NtnTypeBinderList -> assert false)
     metas ([],[])
 
 let match_notation_constr_cases_pattern c (metas,pat) =
-  let vars = List.map fst metas in
-  let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
+  let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in
   reorder_canonically_substitution terms termlists metas, more_args
 
 let match_notation_constr_ind_pattern ind args (metas,pat) =
-  let vars = List.map fst metas in
-  let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in
+  let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in
   reorder_canonically_substitution terms termlists metas, more_args
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c6770deea2..280ccfd21f 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index cb12b98aec..37bbe0ce87 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 0385eea278..de7a42eee5 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3100298e55..7e42c1a227 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 6cae2b0262..9c77400da2 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index ce3c9b8f62..1f28ba6569 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 68ef6594f7..0749ca5769 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e155a5217d..244cdd0a70 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,22 +9,21 @@
 open Genarg
 
 let wit_unit : unit uniform_genarg_type =
-  make0 None "unit"
+  make0 "unit"
 
 let wit_bool : bool uniform_genarg_type =
-  make0 None "bool"
+  make0 "bool"
 
 let wit_int : int uniform_genarg_type =
-  make0 None "int"
+  make0 "int"
 
 let wit_string : string uniform_genarg_type =
-  make0 None "string"
+  make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 None "preident"
+  make0 "preident"
 
-let () = register_name0 wit_unit "Stdarg.wit_unit"
-let () = register_name0 wit_bool "Stdarg.wit_bool"
-let () = register_name0 wit_int "Stdarg.wit_int"
-let () = register_name0 wit_string "Stdarg.wit_string"
-let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+(** Aliases for compatibility *)
+
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 5a44b1ca65..e1f648d7fc 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
 val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d2709d5e3c..db548ec326 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index e5a3f4ceb7..7a1c9c5cb4 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1231f11555..e569f543b5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,14 +19,14 @@ open Constrexpr_ops
 (*i*)
 
 
-let oldfashion_patterns = ref (false)
+let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
   Goptions.optname =
     "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
   Goptions.optkey = ["Asymmetric";"Patterns"];
-  Goptions.optread = (fun () -> !oldfashion_patterns);
-  Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
+  Goptions.optread = (fun () -> !asymmetric_patterns);
+  Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
 }
 
 (**********************************************************************)
@@ -38,27 +38,11 @@ let error_invalid_pattern_notation loc =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-let ids_of_cases_indtype =
-  let rec vars_of ids = function
-    (* We deal only with the regular cases *)
-    | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) ->
-      List.fold_left vars_of (List.fold_left vars_of [] l2) l1
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CPatDelimiters(_,_,c) -> vars_of ids c
-    | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids
-    | _ -> ids in
-  vars_of []
-
-let ids_of_cases_tomatch tms =
-  List.fold_right
-    (fun (_,(ona,indnal)) l ->
-      Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (Option.fold_right (Loc.down_located name_cons) ona l))
-    tms []
-
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
-  with Not_found -> true
+  try Globnames.isConstructRef
+        (Smartlocate.global_of_extended_global
+           (Nametab.locate_extended (qualid_of_ident id)))
+  with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
@@ -68,7 +52,7 @@ let rec cases_pattern_fold_names f a = function
       List.fold_left (cases_pattern_fold_names f) a patl
   | CPatCstr (_,_,patl1,patl2) ->
     List.fold_left (cases_pattern_fold_names f)
-      (List.fold_left (cases_pattern_fold_names f) a patl1) patl2
+      (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
   | CPatNotation (_,_,(patl,patll),patl') ->
       List.fold_left (cases_pattern_fold_names f)
 	(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
@@ -82,6 +66,17 @@ let ids_of_pattern_list =
       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
     Id.Set.empty
 
+let ids_of_cases_indtype p =
+  Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p)
+
+let ids_of_cases_tomatch tms =
+  List.fold_right
+    (fun (_, ona, indnal) l ->
+      Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+      indnal
+        (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
+    tms Id.Set.empty
+
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
@@ -116,11 +111,11 @@ let fold_constr_expr_with_binders g f n acc = function
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
       acc
-  | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+  | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
-      let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
-      let acc = List.fold_left (f n) acc (List.map fst al) in
+      let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
+      let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
@@ -218,13 +213,14 @@ let map_constr_expr_with_binders g f e = function
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _
   | CPrim _ | CRef _ as x -> x
-  | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
+  | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
-      (* TODO: apply g on the binding variables in pat... *)
-      let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+      let bl = List.map (fun (loc,patl,rhs) ->
+        let ids = ids_of_pattern_list patl in
+        (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
-      let po = Option.map (f (List.fold_right g ids e)) rtnpo in
-      CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+      let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
+      CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
       let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b25d7082c1..0f30135f89 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,7 +12,7 @@ open Constrexpr
 
 (** Topconstr *)
 
-val oldfashion_patterns : bool ref
+val asymmetric_patterns : bool ref
 
 (** Utilities on constr_expr *)