Merge branch 'v8.6'

31 files changed, 914 insertions, 182 deletions

diff --git a/CHANGES b/CHANGES
index 8e9bcaba6d..b4e98a0b13 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,6 @@
 Changes beyond V8.5
 ===================
+
 Bugfixes
 
 - #4527: when typechecking the statement of a lemma using universe polymorphic
@@ -9,6 +10,9 @@ Bugfixes
   compatible).
 - #4726: treat user-provided sorts of universe polymorphic records as rigid
   (i.e. non-minimizable).
+- #4592, #4932: notations sharing recursive patterns or sharing
+  binders made more robust.
+- #4780: Induction with universe polymorphism on was creating ill-typed terms.
 
 Specification language
 
@@ -79,6 +83,10 @@ Tools
   computation associated with printing the "dependent evars: " line in
   -emacs mode
 
+Changes from V8.5pl2 to V8.5pl3
+===============================
+- #4780: Induction with universe polymorphism on was creating ill-typed terms.
+
 Changes from V8.5pl1 to V8.5pl2
 ===============================
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 023835af76..e09477014b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,8 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
-let pp   x = Feedback.msg_notice x
-let pppp x = Feedback.msg_notice x
+let pp   x = Pp.pp_with !Pp_control.std_ft x
 
 (** Future printer *)
 
@@ -316,7 +315,7 @@ let constr_display csr =
     | Anonymous -> "Anonymous"
 
   in
-  Feedback.msg_notice (str (term_display csr) ++fnl ())
+  pp (str (term_display csr) ++fnl ())
 
 open Format;;
 
@@ -514,7 +513,7 @@ let _ =
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Feedback.msg_notice (CErrors.print e)
+    e -> pp (CErrors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
@@ -530,7 +529,7 @@ let _ =
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Feedback.msg_notice (CErrors.print e)
+    e -> pp (CErrors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index e91480ded3..92107b750b 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -589,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
   (t at level 39).
 \end{coq_example*}
 
+Recursive patterns can occur several times on the right-hand side.
+Here is an example:
+
+\begin{coq_example*}
+Notation "[> a , .. , b <]" :=
+  (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+\end{coq_example*}
+
 Notations with recursive patterns can be reserved like standard
 notations, they can also be declared within interpretation scopes (see
 section \ref{scopes}).
@@ -634,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders:
 \begin{coq_example*}
 Notation "'mylet' f x .. y :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (x closed binder, y closed binder, at level 200, right associativity).
+  (at level 200, x closed binder, y closed binder, right associativity).
+\end{coq_example*}
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+\begin{coq_example*}
+Notation ``'FUNAPP' x .. y , f'' :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
 \subsection{Summary}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7476871890..e71daef999 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -848,10 +848,11 @@ and extern_local_binder scopes vars = function
   | (Inr p,bk,Some bd,ty)::l -> assert false
 
   | (Inr p,bk,None,ty)::l ->
-      let ty = extern_typ scopes vars ty in
+      let ty =
+        if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l)
+      (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 438aa2f7c6..fb1baae0a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -604,31 +604,52 @@ let rec subordinate_letins intern letins = function
   | [] ->
       letins,[]
 
-let rec subst_iterator y t = function
-  | GVar (_,id) as x -> if Id.equal id y then t else x
-  | x -> map_glob_constr (subst_iterator y t) x
+let terms_of_binders bl =
+  let rec term_of_pat = function
+    | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
+    | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
+    | PatCstr (loc,c,l,_) ->
+       let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
+       let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+       let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+       CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+  let rec extract_variables = function
+    | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l
+    | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l
+    | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term."
+    | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l
+    | [] -> [] in
+  extract_variables bl
 
 let instantiate_notation_constr loc intern ntnvars subst infos c =
   let (terms,termlists,binders) = subst in
   (* when called while defining a notation, avoid capturing the private binders
      of the expression by variables bound by the notation (see #3892) *)
   let avoid = Id.Map.domain ntnvars in
-  let rec aux (terms,binderopt as subst') (renaming,env) c =
+  let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c =
     let subinfos = renaming,{env with tmp_scope = None} in
     match c with
+    | NVar id when Id.equal id ldots_var -> Option.get terminopt
     | NVar id -> subst_var subst' (renaming, env) id
-    | NList (x,_,iter,terminator,lassoc) ->
-      (try
+    | NList (x,y,iter,terminator,lassoc) ->
+      let l,(scopt,subscopes) =
         (* All elements of the list are in scopes (scopt,subscopes) *)
-	let (l,(scopt,subscopes)) = Id.Map.find x termlists in
-        let termin = aux subst' subinfos terminator in
-        let fold a t =
-          let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in
-          subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter)
-        in
-	List.fold_right fold (if lassoc then List.rev l else l) termin
-      with Not_found ->
-          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
+        try
+          let l,scopes = Id.Map.find x termlists in
+          (if lassoc then List.rev l else l),scopes
+        with Not_found ->
+        try
+	  let (bl,(scopt,subscopes)) = Id.Map.find x binders in
+	  let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+          terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[])
+        with Not_found ->
+          anomaly (Pp.str "Inconsistent substitution of recursive notation") in
+      let termin = aux (terms,None,None) subinfos terminator in
+      let fold a t =
+        let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
+        aux (nterms,None,Some t) subinfos iter
+      in
+      List.fold_right fold l termin
     | NHole (knd, naming, arg) ->
       let knd = match knd with
       | Evar_kinds.BinderType (Name id as na) ->
@@ -663,16 +684,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         Some arg
       in
       GHole (loc, knd, naming, arg)
-    | NBinderList (x,_,iter,terminator) ->
+    | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
 	let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
 	let letins,bl = subordinate_letins intern [] bl in
-        let termin = aux subst' (renaming,env) terminator in
+        let termin = aux (terms,None,None) (renaming,env) terminator in
 	let res = List.fold_left (fun t binder ->
-          subst_iterator ldots_var t
-	    (aux (terms,Some(x,binder)) subinfos iter))
+	    aux (terms,Some(y,binder),Some t) subinfos iter)
 	  termin bl in
 	make_letins letins res
       with Not_found ->
@@ -700,7 +720,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     | t ->
       glob_constr_of_notation_constr_with_binders loc
         (traverse_binder subst avoid) (aux subst') subinfos t
-  and subst_var (terms, binderopt) (renaming, env) id =
+  and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
     try
@@ -713,7 +733,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     with Not_found ->
       (* Happens for local notation joint with inductive/fixpoint defs *)
       GVar (loc,id)
-  in aux (terms,None) infos c
+  in aux (terms,None,None) infos c
 
 let split_by_type ids =
   List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
@@ -1329,7 +1349,7 @@ let drop_notations_pattern looked_for =
       RCPatCstr (loc, g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
-    | NList (x,_,iter,terminator,lassoc) ->
+    | NList (x,y,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.");
       (try
@@ -1337,7 +1357,7 @@ let drop_notations_pattern looked_for =
 	 let (l,(scopt,subscopes)) = Id.Map.find x substlist in
          let termin = in_not top loc scopes fullsubst [] terminator in
 	 List.fold_right (fun a t ->
-           let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in
+           let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in
            let u = in_not false loc scopes (nsubst, substlist) [] iter in
            subst_pat_iterator ldots_var t u)
            (if lassoc then List.rev l else l) termin
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 198bd2216a..6478ade61a 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -237,7 +237,9 @@ let check_is_hole id = function GHole _ -> () | t ->
     strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
 
-let compare_recursive_parts found f (iterator,subc) =
+let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
+
+let compare_recursive_parts found f f' (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
   let rec aux c1 c2 = match c1,c2 with
@@ -284,16 +286,26 @@ let compare_recursive_parts found f (iterator,subc) =
 	user_err_loc (subtract_loc loc1 loc2,"",
           str "Both ends of the recursive pattern are the same.")
     | Some (x,y,Some lassoc) ->
-	let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+        let newfound,x,y,lassoc =
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
+             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
+          then
+            !found,x,y,lassoc
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
+                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
+          then
+            !found,y,x,not lassoc
+          else
+            (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
 	let iterator =
-	  f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
-	  else iterator) in
+	  f' (if lassoc then iterator
+	      else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,None) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
-	let iterator = f iterator in
+	let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NBinderList (x,y,iterator,f (Option.get !terminator))
@@ -305,7 +317,7 @@ let notation_constr_and_vars_of_glob_constr a =
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
-    try compare_recursive_parts found aux' (split_at_recursive_part c)
+    try compare_recursive_parts found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
     match c with
@@ -357,8 +369,6 @@ let notation_constr_and_vars_of_glob_constr a =
   (* Side effect *)
   t, !found
 
-let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
-
 let check_variables nenv (found,foundrec,foundrecbinding) =
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
@@ -585,6 +595,10 @@ let rec alpha_var id1 id2 = function
   | _::idl -> alpha_var id1 id2 idl
   | [] -> Id.equal id1 id2
 
+let alpha_rename alpmetas v =
+  if alpmetas == [] then v
+  else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
+
 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 ..."
@@ -610,16 +624,29 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
      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;
+  let v = alpha_rename alpmetas v in
   (* TODO: handle the case of multiple occs in different scopes *)
   ((var,v)::terms,onlybinders,termlists,binderlists)
 
+let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl =
+  if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
+  let vl = List.map (alpha_rename alpmetas) vl in
+  (terms,onlybinders,(var,vl)::termlists,binderlists)
+
 let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
   (* TODO: handle the case of multiple occs in different scopes *)
   (terms,(var,v)::onlybinders,termlists,binderlists)
 
 let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
-  (terms,onlybinders,termlists,(x,List.rev bl)::binderlists)
+  (terms,onlybinders,termlists,(x,bl)::binderlists)
+
+let rec pat_binder_of_term = function
+  | GVar (loc, id) -> PatVar (loc, Name id)
+  | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
+     let nparams = Inductiveops.inductive_nparams (fst cstr) in
+     let _,l = List.chop nparams l in
+     PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous)
+  | _ -> raise No_match
 
 let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
@@ -630,10 +657,53 @@ let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) 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 sigma
+        if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma
         else raise No_match
   with Not_found -> add_env alp sigma var v
 
+let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
+  try
+    let vl' = Id.List.assoc var termlists in
+    let unify_term v v' =
+      match v, v' with
+      | GHole _, _ -> v'
+      | _, GHole _ -> v
+      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
+    let rec unify vl vl' =
+      match vl, vl' with
+      | [], [] -> []
+      | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl'
+      | _ -> raise No_match in
+    let vl = unify vl vl' in
+    let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
+    add_termlist_env alp sigma var vl
+  with Not_found -> add_termlist_env alp sigma var vl
+
+let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+  try
+    match Id.List.assoc var terms with
+    | GVar (_,id') ->
+       (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
+       sigma
+    | _ -> anomaly (str "A term which can be a binder has to be a variable")
+  with Not_found ->
+    (* The matching against a term allowing to find the instance has not been found yet *)
+    (* If it will be a different name, we shall unfortunately fail *)
+    (* TODO: look at the consequences for alp *)
+    alp, add_env alp sigma var (GVar (Loc.ghost,id))
+
+let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+  try
+    let v' = Id.List.assoc var onlybinders in
+    match v' with
+    | Anonymous ->
+        (* Should not occur, since the term has to be bound upwards *)
+        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+        add_binding_env alp sigma var (Name id)
+    | Name id' ->
+        if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match
+  with Not_found -> add_binding_env alp sigma var (Name id)
+
 let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
     let v' = Id.List.assoc var onlybinders in
@@ -647,6 +717,109 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var
         else (fst alp,(id1,id2)::snd alp),sigma
   with Not_found -> alp, add_binding_env alp sigma var v
 
+let rec map_cases_pattern_name_left f = function
+  | PatVar (loc,na) -> PatVar (loc,f na)
+  | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na)
+
+let rec fold_cases_pattern_eq f x p p' = match p, p' with
+  | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na)
+  | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' ->
+     let x,l = fold_cases_pattern_list_eq f x l l' in
+     let x,na = f x na na' in
+     x, PatCstr (loc,c,l,na)
+  | _ -> failwith "Not equal"
+
+and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
+  | [], [] -> x, []
+  | p::pl, p'::pl' ->
+     let x, p = fold_cases_pattern_eq f x p p' in
+     let x, pl = fold_cases_pattern_list_eq f x pl pl' in
+     x, p :: pl
+  | _ -> assert false
+
+let rec cases_pattern_eq p1 p2 = match p1, p2 with
+| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
+| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
+  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+  Name.equal na1 na2
+| _ -> false
+
+let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
+  let bl = List.rev bl in
+  try
+    let bl' = Id.List.assoc var binderlists in
+    let unify_name alp na na' =
+      match na, na' with
+      | Anonymous, na' -> alp, na'
+      | na, Anonymous -> alp, na
+      | Name id, Name id' ->
+         if Id.equal id id' then alp, na'
+         else (fst alp,(id,id')::snd alp), na' in
+    let unify_pat alp p p' =
+      try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
+    let unify_term alp v v' =
+      match v, v' with
+      | GHole _, _ -> v'
+      | _, GHole _ -> v
+      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
+    let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
+    let unify_binder alp b b' =
+      match b, b' with
+      | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
+         let alp, na = unify_name alp na na' in
+         alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
+      | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
+         let alp, na = unify_name alp na na' in
+         alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
+      | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
+         let alp, p = unify_pat alp p p' in
+         alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+      | _ -> raise No_match in
+    let rec unify alp bl bl' =
+    match bl, bl' with
+    | [], [] -> alp, []
+    | b :: bl, b' :: bl' ->
+       let alp,b = unify_binder alp b b' in
+       let alp,bl = unify alp bl bl' in
+       alp, b :: bl
+    | _ -> raise No_match in
+    let alp, bl = unify alp bl bl' in
+    let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+    alp, add_bindinglist_env sigma var bl
+  with Not_found ->
+    alp, add_bindinglist_env sigma var bl
+
+let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl =
+  try
+    let bl' = Id.List.assoc var binderlists in
+    let unify_id id na' =
+      match na' with
+      | Anonymous -> Name (rename_var (snd alp) id)
+      | Name id' ->
+         if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
+    let unify_pat p p' =
+      if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
+      else raise No_match in
+    let unify_term_binder c b' =
+      match c, b' with
+      | GVar (_, id), (Inl na', bk', None, t') (* assum *) ->
+         (Inl (unify_id id na'), bk', None, t')
+      | c, (Inr p', bk', None, t') (* pattern *) ->
+         let p = pat_binder_of_term c in
+         (Inr (unify_pat p p'), bk', None, t')
+      | _ -> raise No_match in
+    let rec unify cl bl' =
+    match cl, bl' with
+    | [], [] -> []
+    | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl'
+    | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
+    | _ -> raise No_match in
+    let bl = unify cl bl' in
+    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+    add_bindinglist_env sigma var bl
+  with Not_found ->
+    anomaly (str "There should be a binder list bindings this list of terms")
+
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
   | GCoFix n1, GCoFix n2 -> Int.equal n1 n2
@@ -670,8 +843,8 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
       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
+      (* alpha-conversion for the given occurrence of the name (see #4592)) *)
+      bind_term_as_binding_env alp sigma id2 id1
   | (Anonymous,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs *)
       alp, sigma
@@ -691,8 +864,14 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
+  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      when islambda && Id.equal p e ->
+      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GLambda (_,na,bk,t,b) when islambda ->
       match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
+  | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      when not islambda && Id.equal p e ->
+      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
   | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
       match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
@@ -703,35 +882,51 @@ let rec match_iterated_binders islambda decls = function
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
   (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
 
+let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
+  (terms,onlybinders,termlists,Id.List.remove_assoc x 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 =
+let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
+  let rec aux sigma bl rest =
     try
-      let (terms,_,_,binderlists as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let metas = add_ldots_var (add_meta_bindinglist y metas) in
+      let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
       let rest = Id.List.assoc ldots_var terms in
       let b =
-        match Id.List.assoc x binderlists with [b] -> b | _ ->assert false
+        match Id.List.assoc y 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
-  add_bindinglist_env sigma x bl
+      let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
+      aux sigma (b::bl) rest
+    with No_match when not (List.is_empty bl) ->
+      bl, rest, sigma in
+  let bl,rest,sigma = aux sigma [] rest in
+  let alp,sigma = bind_bindinglist_env alp sigma x bl in
+  match_fun alp metas sigma rest termin
+
+let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
 
-let match_alist match_fun metas sigma rest x iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
   let rec aux sigma acc rest =
     try
-      let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in
+      let metas = add_ldots_var (add_meta_term y metas) in
+      let (terms,_,_,_ as sigma) = match_fun 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
+      let t = Id.List.assoc y terms in
+      let sigma = remove_sigma y (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,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
+  let l = if lassoc then l else List.rev l in
+  if is_bindinglist_meta x metas then
+    (* This is a recursive pattern for both bindings and terms; it is *)
+    (* registered for binders *)
+    bind_bindinglist_as_term_env alp sigma x l
+  else
+    bind_termlist_env alp sigma x l
 
 let does_not_come_from_already_eta_expanded_var =
   (* This is hack to avoid looping on a rule with rhs of the form *)
@@ -750,46 +945,58 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
-  | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> snd (bind_binding_env alp sigma id2 (Name id1))
+  | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+  | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
-  | r1, NList (x,_,iter,termin,lassoc) ->
-      match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
+  | r1, NList (x,y,iter,termin,lassoc) ->
+      match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
-    NBinderList (x,_,NLambda (Name id2,_,b2),(NVar v as termin)) when p = e ->
-      let decls = [(Inr cp,bk,None,t1)] in
-      match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
+      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let alp,sigma = bind_bindinglist_env alp sigma x decls in
+      match_in u alp metas sigma b termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
+  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
       let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
-      match_in u alp metas (add_bindinglist_env sigma x decls) b termin
+      let alp,sigma = bind_bindinglist_env alp sigma x decls in
+      match_in u alp metas sigma b termin
 
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],t)])),
-    NBinderList (x,_,NProd (Name id2,_,b2),(NVar v as termin)) when p = e ->
-      let decls = [(Inr cp,bk,None,t1)] in
-      match_in u alp metas (add_bindinglist_env sigma x decls) t termin
+  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
+      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let alp,sigma = bind_bindinglist_env alp sigma x decls in
+      match_in u alp metas sigma b termin
 
-  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
+  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
       let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
-      match_in u alp metas (add_bindinglist_env sigma x decls) b termin
+      let alp,sigma = bind_bindinglist_env alp sigma x decls in
+      match_in u alp metas sigma 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
+  | r, NBinderList (x,y,iter,termin) ->
+      match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
+  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+    NLambda (Name id,_,b2)
+      when is_bindinglist_meta id metas ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in
+      match_in u alp metas sigma 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 [(Inl na,bk,None,t)]) b1 b2
+      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      match_in u alp metas sigma b1 b2
   | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
-      match_in u alp metas (add_bindinglist_env sigma id [(Inl na,bk,None,t)]) b1 b2
+      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
   | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
@@ -876,7 +1083,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          alp, add_bindinglist_env sigma id [(Inl (Name id'),Explicit,None,t1)]
+          bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
@@ -944,6 +1151,20 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::terms,x,termlists,y
 
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
+  let rec aux sigma acc rest =
+    try
+      let metas = add_ldots_var (add_meta_term y metas) in
+      let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
+      let rest = Id.List.assoc ldots_var terms in
+      let t = Id.List.assoc y terms in
+      let sigma = remove_sigma y (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,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+  (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
+
 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_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
@@ -960,9 +1181,9 @@ let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
       else
 	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 (match_cases_pattern_no_more_args)
-	metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[])
+  | r1, NList (x,y,iter,termin,lassoc) ->
+      (match_cases_pattern_list (match_cases_pattern_no_more_args)
+	metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8ecc7d015a..199ef9fcee 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -490,9 +490,6 @@ GEXTEND Gram
     [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
     | -> None ] ]
   ;
-  rename :
-    [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
-  ;
   rewriter :
     [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
       | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
@@ -518,12 +515,6 @@ GEXTEND Gram
         | _,_,Some _ -> err ()
         | _,_,None -> (ic,el) ]]
   ;
-  move_location:
-    [ [ IDENT "after"; id = id_or_meta -> MoveAfter id
-      | IDENT "before"; id = id_or_meta -> MoveBefore id
-      | "at"; IDENT "top" -> MoveFirst
-      | "at"; IDENT "bottom" -> MoveLast ] ]
-  ;
   simple_tactic:
     [ [
       (* Basic tactics *)
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index a19e9df904..7e3ef89293 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -93,7 +93,7 @@ End S.
 Ltac jump_simpl :=
   repeat
     match goal with
-      | |- appcontext [jump xH] => rewrite (jump_simpl xH)
-      | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
-      | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
+      | |- context [jump xH] => rewrite (jump_simpl xH)
+      | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p))
+      | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p))
     end.
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5c8060996a..51660818f4 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -470,6 +470,78 @@ let loc_of_glob_constr = function
   | GCast (loc,_,_) -> loc
 
 (**********************************************************************)
+(* Alpha-renaming                                                     *)
+
+let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
+let test_id l id = if collide_id l id then raise Not_found
+let test_na l na = name_iter (test_id l) na
+
+let update_subst na l =
+  let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
+  let l' = name_fold Id.List.remove_assoc na l in
+  name_fold
+    (fun id _ ->
+     if in_range id l' then
+       let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
+       Name id', (id,id')::l
+     else na,l)
+    na (na,l)
+
+exception UnsoundRenaming
+
+let rename_var l id =
+  try
+    let id' = Id.List.assoc id l in
+    (* Check that no other earlier binding hide the one found *)
+    let _,(id'',_) = List.extract_first (fun (_,id) -> Id.equal id id') l in
+    if Id.equal id id'' then id' else raise UnsoundRenaming
+  with Not_found ->
+    if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
+    else id
+
+let rec rename_glob_vars l = function
+  | GVar (loc,id) as r ->
+      let id' = rename_var l id in
+      if id == id' then r else GVar (loc,id')
+  | GRef (_,VarRef id,_) as r ->
+      if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
+      else r
+  | GProd (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLambda (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLetIn (loc,na,b,c) ->
+      let na',l' = update_subst na l in
+      GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c)
+  (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
+  | GCases (loc,ci,po,tomatchl,cls) ->
+      let test_pred_pat (na,ino) =
+        test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in
+      let test_clause idl = List.iter (test_id l) idl in
+      let po = Option.map (rename_glob_vars l) po in
+      let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
+      let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in
+      GCases (loc,ci,po,tomatchl,cls)
+  | GLetTuple (loc,nal,(na,po),c,b) ->
+     List.iter (test_na l) (na::nal);
+     GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po),
+                rename_glob_vars l c,rename_glob_vars l b)
+  | GIf (loc,c,(na,po),b1,b2) ->
+     test_na l na;
+     GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
+          rename_glob_vars l b1,rename_glob_vars l b2)
+  | GRec (loc,k,idl,decls,bs,ts) ->
+     Array.iter (test_id l) idl;
+     GRec (loc,k,idl,
+           Array.map (List.map (fun (na,k,bbd,bty) ->
+             test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
+           Array.map (rename_glob_vars l) bs,
+           Array.map (rename_glob_vars l) ts)
+  | r -> map_glob_constr (rename_glob_vars l) r
+
+(**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
 let rec cases_pattern_of_glob_constr na = function
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c2b27ca6ab..55e6b6533f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -44,6 +44,16 @@ val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
 val glob_visible_short_qualid : glob_constr -> Id.t list
 
+(* Renaming free variables using a renaming map; fails with
+   [UnsoundRenaming] if applying the renaming would introduce
+   collision, as in, e.g., renaming [P x y] using substitution [(x,y)];
+   inner alpha-conversion done only for forall, fun, let but
+   not for cases and fix *)
+
+exception UnsoundRenaming
+val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t
+val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr
+
 (** [map_pattern_binders f m c] applies [f] to all the binding names
     in a pattern-matching expression ({!Glob_term.GCases}) represented
     here by its relevant components [m] and [c]. It is used to
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 252b0967dc..935e2d076e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -349,8 +349,13 @@ end) = struct
         | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
-    | LocalPattern _ ->
-      assert false
+    | LocalPattern (loc,p,tyo) ->
+      let p = pr_patt lsimplepatt p in
+      match tyo with
+        | None ->
+          str "'" ++ p
+        | Some ty ->
+          str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
 
   let pr_undelimited_binders sep pr_c =
     prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -360,10 +365,8 @@ end) = struct
     match bl with
       | [LocalRawAssum (nal,k,t)] ->
         pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
-      | LocalRawAssum _ :: _ as bdl ->
+      | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
         pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
-      | LocalPattern (loc,p,tyo) :: _ ->
-        str "'" ++ pr_patt ltop p
       | _ -> assert false
 
   let pr_binders_gen pr_c sep is_open =
@@ -376,6 +379,11 @@ end) = struct
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
     | CProdN (loc,[],c) ->
       extract_prod_binders c
+    | CProdN (loc,[[_,Name id],bk,t],
+              CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+         when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+      let bl,c = extract_prod_binders b in
+      LocalPattern (loc,p,None) :: bl, c
     | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -387,6 +395,11 @@ end) = struct
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
     | CLambdaN (loc,[],c) ->
       extract_lam_binders c
+    | CLambdaN (loc,[[_,Name id],bk,t],
+                CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+         when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+      let bl,c = extract_lam_binders b in
+      LocalPattern (loc,p,None) :: bl, c
     | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -538,21 +551,6 @@ end) = struct
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
           lfix
         )
-      | CProdN
-          (_,
-           [([(_,Name n)],_,_)],
-           CCases
-             (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)],
-              [(_,[(_,[p])],a)]))
-          when
-            Id.equal m n &&
-            not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) ->
-        return (
-          hov 0 (
-            keyword "forall" ++ spc () ++ str "'" ++ pr_patt ltop p ++
-            str "," ++ pr spc ltop a),
-          llambda
-        )
       | CProdN _ ->
         let (bl,a) = extract_prod_binders a in
         return (
@@ -562,21 +560,6 @@ end) = struct
               str "," ++ pr spc ltop a),
           lprod
         )
-      | CLambdaN
-          (_,
-           [([(_,Name n)],_,_)],
-           CCases
-             (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)],
-              [(_,[(_,[p])],a)]))
-          when
-            Id.equal m n &&
-            not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) ->
-        return (
-          hov 0 (
-            keyword "fun" ++ spc () ++ str "'" ++ pr_patt ltop p ++
-            pr_fun_sep ++ pr spc ltop a),
-          llambda
-        )
       | CLambdaN _ ->
         let (bl,a) = extract_lam_binders a in
         return (
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e489013143..38af9a0caa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2665,10 +2665,15 @@ let letin_tac with_eq id c ty occs =
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
     let abs = AbstractExact (id,c,ty,occs,true) in
-    let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in
-    (* We keep the original term to match *)
+    let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
+    (* We keep the original term to match but record the potential side-effects
+       of unifying universes. *)
+    let Sigma (c, sigma, p) = match res with
+      | None -> Sigma.here c sigma
+      | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p)
+    in
     let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in
-    Sigma.here tac sigma
+    Sigma (tac, sigma, p)
   end }
 
 let letin_pat_tac with_eq id c occs =
diff --git a/test-suite/bugs/closed/2839.v b/test-suite/bugs/closed/2839.v
index e396fe06e5..e727e26061 100644
--- a/test-suite/bugs/closed/2839.v
+++ b/test-suite/bugs/closed/2839.v
@@ -5,6 +5,6 @@ intro.
 Fail
   let H :=
     match goal with
-    | [ H : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
+    | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
     end
   in pose H.
diff --git a/test-suite/bugs/closed/3383.v b/test-suite/bugs/closed/3383.v
new file mode 100644
index 0000000000..25257644a6
--- /dev/null
+++ b/test-suite/bugs/closed/3383.v
@@ -0,0 +1,6 @@
+Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end.
+intro.
+lazymatch goal with
+| [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ]
+  => change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b)
+end.
diff --git a/test-suite/bugs/closed/3563.v b/test-suite/bugs/closed/3563.v
index 679721667a..961563ed4a 100644
--- a/test-suite/bugs/closed/3563.v
+++ b/test-suite/bugs/closed/3563.v
@@ -16,11 +16,11 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> H * H0)
        transport (fun y : H1 -> H * H0 => H5 (fst (y H2))) H4 H6 = H7.
   intros.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
+    | [ |- context ctx [transport (fun y => (?g (@fst ?C ?h (y H2)))) H4 H6] ]
       => set(foo:=h); idtac
   end.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (fst (y H2))))] ]
+    | [ |- context ctx [transport (fun y => (?g (fst (y H2))))] ]
       => idtac
   end.
 Abort.
@@ -30,7 +30,7 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0)
        transport (fun y : H1 -> (H1 -> H) * H0 => H5 (fst (y H2) H2)) H4 H6 = H7.
   intros.
   match goal with
-    | [ |- appcontext ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ]
+    | [ |- context ctx [transport (fun y => (?g (@fst ?C ?D (y H2) ?X)))] ]
       => set(foo:=X)
   end.
 (* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index f85a60264d..eb37141bcf 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -11,7 +11,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   simpl.
   intros.
   match goal with
-    | [ |- appcontext G[@hd] ] => idtac
+    | [ |- context G[@hd] ] => idtac
   end.
 
 (* This second example comes from CFGV where inspecting subterms of a
diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v
new file mode 100644
index 0000000000..4cec43184c
--- /dev/null
+++ b/test-suite/bugs/closed/4780.v
@@ -0,0 +1,106 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *)
+(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3
+   coqtop version 8.5pl1 (April 2016) *)
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+Global Set Universe Polymorphism.
+Global Set Asymmetric Patterns.
+Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
+  (at level 200, x binder, right associativity,
+   format "'[' 'exists'  '/  ' x  ..  y ,  '/  ' p ']'")
+  : type_scope.
+Definition relation (A : Type) := A -> A -> Type.
+Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z.
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  refine (@transitivity _ R _ x y z _ _).
+Tactic Notation "etransitivity" := etransitivity _.
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Notation "x .2" := (projT2 x) (at level 3) : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Arguments paths_rect [A] a P f y p.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Instance transitive_paths {A} : Transitive (@paths A) | 0 := @concat A.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Notation "1" := idpath : path_scope.
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+Notation "p ^" := (inverse p) (at level 3) : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y
+  := match p with idpath => idpath end.
+Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
+  (p : x = y) (z : P (f x))
+  : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+admit.
+Defined.
+Local Open Scope path_scope.
+Generalizable Variables X A B C f g n.
+Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+  (pq : {p : u.1 = v.1 &  p # u.2 = v.2})
+  : u = v
+  := match pq with
+       | existT p q =>
+         match u, v return (forall p0 : (u.1 = v.1), (p0 # u.2 = v.2) -> (u=v)) with
+           | (x;y), (x';y') => fun p1 q1 =>
+             match p1 in (_ = x'') return (forall y'', (p1 # y = y'') -> (x;y)=(x'';y'')) with
+               | idpath => fun y' q2 =>
+                 match q2 in (_ = y'') return (x;y) = (x;y'') with
+                   | idpath => 1
+                 end
+             end y' q1
+         end p q
+     end.
+Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P)
+  (p : u.1 = v.1) (q : p # u.2 = v.2)
+  : u = v
+  := path_sigma_uncurried P u v (p;q).
+Definition projT1_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+  : u.1 = v.1
+  :=
+  ap (@projT1 _ _) p.
+Notation "p ..1" := (projT1_path p) (at level 3) : fibration_scope.
+Definition projT2_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+  : p..1 # u.2 = v.2
+  := (transport_compose P (@projT1 _ _) p u.2)^
+     @ (@apD {x:A & P x} _ (@projT2 _ _) _ _ p).
+Notation "p ..2" := (projT2_path p) (at level 3) : fibration_scope.
+Definition eta_path_sigma_uncurried `{P : A -> Type} {u v : sigT P}
+  (p : u = v)
+  : path_sigma_uncurried _ _ _ (p..1; p..2) = p.
+admit.
+Defined.
+Definition eta_path_sigma `{P : A -> Type} {u v : sigT P} (p : u = v)
+  : path_sigma _ _ _ (p..1) (p..2) = p
+  := eta_path_sigma_uncurried p.
+
+Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+  (p q : u = v)
+  (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2})
+  : p = q.
+Proof.
+  destruct rs, p, u.
+  etransitivity; [ | apply eta_path_sigma ].
+  simpl in *.
+  induction p0.
+  admit.
+Defined.
+
diff --git a/test-suite/bugs/closed/4932.v b/test-suite/bugs/closed/4932.v
new file mode 100644
index 0000000000..219d532ac6
--- /dev/null
+++ b/test-suite/bugs/closed/4932.v
@@ -0,0 +1,44 @@
+(* Testing recursive notations with binders seen as terms *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (
+    (fun x => ..
+                (fun z =>
+                   pack
+                     (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+                     (existT _ x .. (existT _ z tt) .. )
+                ) ..
+    )
+  ) (at level 85, x binder, z binder).
+
+Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt))
+                                   (existT _ (y,z) tt).
+
+Example test := tele (t : Type) := tt.
+Example test' := test nat.
+Print test.
+
+Example test2 := tele (t : Type) (x:t) := tt.
+Example test2' := test2 nat 0.
+Print test2.
+
+Example test3 := tele (t : Type) (y:=0) (x:t) := tt.
+Example test3' := test3 nat 0.
+Print test3.
+
+Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt.
+Example test4' := test4 nat (1,2) 3.
+Print test4.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 008fb72c4e..73da464bbe 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -22,8 +22,8 @@ Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := o
 
 Ltac present_obj from to :=
   match goal with
-           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
-           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
+           | [ _ : context[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
+           | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
          end.
 
 Section NaturalTransformationComposition.
diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v
index 5e5d5ab3e7..3d16e7ac0d 100644
--- a/test-suite/bugs/closed/HoTT_coq_058.v
+++ b/test-suite/bugs/closed/HoTT_coq_058.v
@@ -95,10 +95,10 @@ Goal forall (T : Type) (T0 : T -> T -> Type)
                            | tt => idpath
                          end)) (x1; p) = (x1; p).
 intros.
-let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in
-let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in
-let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in
-let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in
+let F := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in
+let H := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in
+let X := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in
+let T := match goal with |- context[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in
 let t0 := fresh "t0" in
 let t1 := fresh "t1" in
 let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
@@ -116,7 +116,7 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
               let GL1' := fresh in
               set (GL0' := GL0);
 
-                let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in
+                let arg := match GL0 with context[x0 ?arg] => constr:(arg) end in
                 assert (t1 = arg) by (subst t1; reflexivity); subst t1;
                 pattern (x0 arg) in GL0';
                 match goal with
diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v
deleted file mode 100644
index 9a14641a57..0000000000
--- a/test-suite/bugs/opened/3383.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end.
-intro.
-Fail lazymatch goal with
-| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ]
-  => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f)
-end. (* Toplevel input, characters 153-154:
-Error: The reference P was not found in the current environment. *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index d9ce42c606..20101f48e5 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
      : nat
 exists myx y : bool, myx = y
      : Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
new file mode 100644
index 0000000000..360f379676
--- /dev/null
+++ b/test-suite/output/Notations3.out
@@ -0,0 +1,100 @@
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+(0, 2, (2, 2))
+     : nat * nat * (nat * nat)
+pair (pair O (S (S O))) (pair (S (S O)) O)
+     : prod (prod nat nat) (prod nat nat)
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (2, (2, 0)))
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (0, (2, 4)))
+     : nat * nat * nat * (nat * (nat * nat))
+pair (pair (pair O (S (S O))) (S (S (S (S O)))))
+  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+     : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+fun x y : nat => Nat.add x y
+     : forall (_ : nat) (_ : nat), nat
+ETA x y : nat, le_S
+     : forall x y : nat, x <= y -> x <= S y
+fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
+     : (forall x : nat * (bool * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
+where
+?T : [x : nat * (bool * unit) |- Type] 
+fun f : forall x : bool * (nat * unit), ?T =>
+CURRYINV (x : nat) (y : bool), f
+     : (forall x : bool * (nat * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
+where
+?T : [x : bool * (nat * unit) |- Type] 
+fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
+     : (forall x : unit * nat * bool, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
+where
+?T : [x : unit * nat * bool |- Type] 
+fun f : forall x : unit * bool * nat, ?T =>
+CURRYINVLEFT (x : nat) (y : bool), f
+     : (forall x : unit * bool * nat, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
+where
+?T : [x : unit * bool * nat |- Type] 
+forall n : nat, {#n | 1 > n}
+     : Prop
+forall x : nat, {|x | x > 0|}
+     : Prop
+exists2 x : nat, x = 1 & x = 2
+     : Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_3
+     : nat -> Prop
+fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_4
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
+     : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+     : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
new file mode 100644
index 0000000000..4b8bfe3124
--- /dev/null
+++ b/test-suite/output/Notations3.v
@@ -0,0 +1,141 @@
+(**********************************************************************)
+(* Check printing of notations with several instances of a recursive pattern *)
+(* Was wrong but I could not trigger a problem due to the collision between *)
+(* different instances of ".." *)
+
+Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)).
+Check [<0,2>].
+Check ((0,2),(2,0)).
+Check ((0,2),(2,2)).
+Unset Printing Notations.
+Check [<0,2>].
+Set Printing Notations.
+
+Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
+Check <<0,2,4>>.
+Check (((0,2),4),(4,(2,0))).
+Check (((0,2),4),(2,(2,0))).
+Check (((0,2),4),(0,(2,4))).
+Unset Printing Notations.
+Check <<0,2,4>>.
+Set Printing Notations.
+
+(**********************************************************************)
+(* Check notations with recursive notations both in binders and terms *)
+
+Notation "'ETA' x .. y , f" :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder).
+Check ETA (x:nat) (y:nat), Nat.add.
+Check ETA (x y:nat), Nat.add.
+Check ETA x y, Nat.add.
+Unset Printing Notations.
+Check ETA (x:nat) (y:nat), Nat.add.
+Set Printing Notations.
+Check ETA x y, le_S.
+
+Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRY (x:nat) (y:bool), f.
+
+Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINV (x:nat) (y:bool), f.
+
+Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYLEFT (x:nat) (y:bool), f.
+
+Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder      *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).
+
+(* Other tests about alpha-conversions: the following notation
+   contains all three kinds of bindings:
+
+   - x is bound in the lhs as a term and a binder: its name is forced
+     by its position as a term; it can bind variables in P
+   - y is bound in the lhs as a binder only: its name is given by its
+     name as a binder in the term to display; it can bind variables in P
+   - z is a binder local to the rhs; it cannot bind a variable in P
+*)
+
+Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)).
+
+(* Not printable: z (resp c, n) occurs in P *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x).
+Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x).
+Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x).
+
+(* Printable *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x).
+
+(* Not printable: renaming x into n would bind the 2nd occurrence of n *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+
+(* Other tests *)
+Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)).
+
+(* Printable *)
+Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo3 n (fun x y z => (fun _ => z=0) z).
+
+(* Not printable: renaming z in n would hide the renaming of x into n *)
+Check fun n => foo3 n (fun x y z => (fun _ => x=0) z).
+
+(* Other tests *)
+Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)).
+
+(* Printable *)
+Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
+
+(* Not printable: y, z not allowed to occur in P *)
+Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
+
+(**********************************************************************)
+(* Test printing of #4932                                             *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (fun x => .. (fun z =>
+     pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+          (existT _ x .. (existT _ z tt) .. )
+                ) ..)
+  (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 6a28475d7b..c012a86b01 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,28 +4,36 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun 'exist _ x _ => x : A
+proj_informative = fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-foo = fun 'Bar n b tt p => if b then n + p else n - p
+foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
 baz = 
-fun 'Bar n1 _ tt p1 => fun 'Bar _ _ tt _ => n1 + p1
+fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-λ '(x, y), (y, x)
-     : A * B → B * A
-∀ '(x, y), swap (x, y) = (y, x)
-     : Prop
 swap = 
-fun (A B : Type) (pat : A * B) => let '(x, y) := pat in (y, x)
+fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
 Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
-forall (A B : Type) (pat : A * B), let '(x, y) := pat in swap (x, y) = (y, x)
+fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
+     : forall A B : Type, A * B -> Prop
+forall (A B : Type) '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y), swap (x, y) = (y, x)
      : Prop
-exists pat : A * A, let '(x, y) := pat in swap (x, y) = (y, x)
+exists '(x, y) '(z, w), swap (x, y) = (z, w)
+     : Prop
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
 fun pat : nat * nat =>
 let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
+fun '(x, y) '(z, t) => swap (x, y) = (z, t)
+     : A * B -> B * A -> Prop
+forall '(x, y) '(z, t), swap (x, y) = (z, t)
+     : Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 8911909abc..b5c91e347b 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -21,7 +21,20 @@ Print foo.
 Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
 Print baz.
 
-(** Some test involving unicode noations. *)
+Module WithParameters.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x).
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w).
+
+End WithParameters.
+
+(** Some test involving unicode notations. *)
 Module WithUnicode.
 
   Require Import Coq.Unicode.Utf8.
@@ -31,24 +44,21 @@ Module WithUnicode.
 
 End WithUnicode.
 
-
 (** * Suboptimal printing *)
 
-(** These tests show examples which expose the [let] introduced by
-    the pattern notation in binders. *)
-
 Module Suboptimal.
 
-Definition swap {A B} '((x,y) : A*B) := (y,x).
-Print swap.
-
-Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
-
-Check exists '((x,y):A*A), swap (x,y) = (y,x).
+(** This test shows an example which exposes the [let] introduced by
+    the pattern notation in binders. *)
 
 Inductive Fin (n:nat) := Z : Fin n.
 Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
 
+(** These tests show examples which do not factorize binders *)
+
+Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
+Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
+
 End Suboptimal.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index b72a067407..2f7c62972a 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l).
 
 Notation "'intros' x" := (S x) (at level 0).
 Goal True -> True. intros H. exact H. Qed.
+
+(* Check absence of collision on ".." in nested notations with ".." *)
+Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index a3eb91ec65..5d1e87ae0c 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -55,12 +55,6 @@ Ltac contradict H :=
    | _ => (elim H;fail) || pos H
   end.
 
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
-
-Ltac swap H :=
-  idtac "swap is OBSOLETE: use contradict instead.";
-  intro; apply H; clear H.
-
 (* To contradict an hypothesis without copying its type. *)
 
 Ltac absurd_hyp H :=
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 985ecaf279..b5b17e5e8d 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -34,7 +34,7 @@ Section Well_founded.
   destruct 1; trivial.
  Defined.
 
- Global Implicit Arguments Acc_inv [x y] [x].
+ Global Arguments Acc_inv [x] _ [y] _, [x] _ y _.
 
  (** A relation is well-founded if every element is accessible *)
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 7384790dae..dfd6b0eae0 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -264,7 +264,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | appcontext [False_rect _ ?p] => elim p
+        | context [False_rect _ ?p] => elim p
       end
   end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a2fd05cd96..c490ea5166 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end