Merge branch 'v8.5'

23 files changed, 264 insertions, 168 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7011f1ef8..bea25a92f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -691,6 +691,13 @@ variables of the form {\tt @?id} that occur in head position of an
 application. For these variables, the matching is second-order and
 returns a functional term.
 
+Alternatively, when a metavariable of the form {\tt ?id} occurs under
+binders, say $x_1$, \ldots, $x_n$ and the expression matches, the
+metavariable is instantiated by a term which can then be used in any
+context which also binds the variables $x_1$, \ldots, $x_n$ with
+same types. This provides with a primitive form of matching
+under context which does not require manipulating a functional term.
+
 If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is
 evaluated into some value by substituting the pattern matching
 instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 5dbf31553..481afa8f8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -165,14 +165,17 @@ in Section~\ref{ProofWith}.
   {\tt Type* } is the forward transitive closure of the entire set of
   section variables occurring in the statement.
 
-\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
 
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
-\variant {\tt Proof using }  {\emph collection$_1$}{\tt* .}
+\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
+
+\variant {\tt Proof using \nterm{collection} * .}
 
   Use section variables being, respectively, in the set union, set difference,
   set complement, set forward transitive closure.
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ce53680f3..45f482cd4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -119,6 +119,7 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
 
+type binding_bound_vars = Id.Set.t
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
 type delayed_open_constr_with_bindings =
@@ -330,7 +331,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_utrm = g_trm
-type g_pat = glob_constr_and_expr * constr_pattern
+type g_pat = glob_constr_pattern_and_expr
 type g_cst = evaluable_global_reference and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam  = Id.t located
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 891d95378..448bf8544 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,13 +17,16 @@ open Term
 
 type tag = int
 
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
+let accu_tag = 0
+
+let max_atom_tag = 1
+let proj_tag = 2
+let fix_app_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
+
+
 (* It would be great if OCaml exported this value,
    So fixme if this happens in a new version of OCaml *)
 let last_variant_tag = 245 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 8f594a45b..03d638305 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -13,13 +13,15 @@ open Term
 
 type tag = int
 
-val id_tag : tag
-val iddef_tag : tag
-val ind_tag : tag
-val fix_tag : tag
+val accu_tag : tag
+
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
+
 val last_variant_tag : tag 
 
 type structured_constant =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a02d5e205..1f8706652 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,10 +165,7 @@ let rec make_subst env =
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-	  if Univ.Universe.is_levels s then
-            make (cons_subst u s subst) (sign, exp, args)
-	  else (* Cannot handle substitution by i+n universes. *)
-	    make subst (sign, exp, args)
+          make (cons_subst u s subst) (sign, exp, args)
     | (na,None,t)::sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fe82d85d5..8895bae5d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -134,10 +134,16 @@ let extract_context_levels env l =
 let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
-  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
-      let param_ccls = extract_context_levels env params in
-      let s = { template_param_levels = param_ccls; template_level = u} in
-      TemplateArity (params,s)
+  | Sort (Type u) ->
+     let ind, l = decompose_app (whd_betadeltaiota env c) in
+     if isInd ind && List.is_empty l then
+       let mis = lookup_mind_specif env (fst (destInd ind)) in
+       let nparams = Inductive.inductive_params mis in
+       let paramsl = CList.lastn nparams params in
+       let param_ccls = extract_context_levels env paramsl in
+       let s = { template_param_levels = param_ccls; template_level = u} in
+       TemplateArity (params,s)
+     else RegularArity t
   | _ ->
       RegularArity t
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 29e2ee601..eacd803fd 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -19,14 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset : Obj.t -> int = "coq_offset"
 
-let accu_tag = 0
-let max_atom_tag = 1
-let proj_tag = 2
-let fix_app_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-
 (*******************************************)
 (* Initalization of the abstract machine ***)
 (*******************************************)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a0493777a..19c85c9e2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -56,10 +56,6 @@ let warn_bound_meta name =
 let warn_bound_bound name =
   msg_warning (str "Collision between bound variables of name " ++ pr_id name)
 
-let warn_bound_again name =
-  msg_warning (str "Collision between bound variable " ++ pr_id name ++
-    str " and another bound variable of same name.")
-
 let constrain n (ids, m as x) (names, terms as subst) =
   try
     let (ids', m') = Id.Map.find n terms in
@@ -69,32 +65,33 @@ let constrain n (ids, m as x) (names, terms as subst) =
     let () = if Id.Map.mem n names then warn_bound_meta n in
     (names, Id.Map.add n x terms)
 
-let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
-| Name id1, Name id2 ->
-  if Id.Map.mem id1 names then
-    let () = warn_bound_bound id1 in
-    (names, terms)
-  else
-    let names = Id.Map.add id1 id2 names in
-    let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
-    (names, terms)
-| _ -> subst
-
-let rec build_lambda vars stk m = match vars with
+let add_binders na1 na2 binding_vars (names, terms as subst) =
+  match na1, na2 with
+  | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
+    if Id.Map.mem id1 names then
+      let () = warn_bound_bound id1 in
+      (names, terms)
+    else
+      let names = Id.Map.add id1 id2 names in
+      let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
+      (names, terms)
+  | _ -> subst
+
+let rec build_lambda vars ctx m = match vars with
 | [] ->
-  let len = List.length stk in
+  let len = List.length ctx in
   lift (-1 * len) m
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length stk in
+  let len = List.length ctx in
   let init i =
     if i < pred n then mkRel (i + 2)
     else if Int.equal i (pred n) then mkRel 1
     else mkRel (i + 1)
   in
   let m = substl (List.init len init) m in
-  let pre, suf = List.chop (pred n) stk in
+  let pre, suf = List.chop (pred n) ctx in
   match suf with
   | [] -> assert false
   | (_, na, t) :: suf ->
@@ -108,21 +105,21 @@ let rec build_lambda vars stk m = match vars with
     let m = mkLambda (na, t, m) in
     build_lambda vars (pre @ suf) m
 
-let rec extract_bound_aux k accu frels stk = match stk with
+let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
-| (na1, na2, _) :: stk ->
+| (na1, na2, _) :: ctx ->
   if Int.Set.mem k frels then
     begin match na1 with
     | Name id ->
       let () = assert (match na2 with Anonymous -> false | Name _ -> true) in
       let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
-      extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk
+      extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
     | Anonymous -> raise PatternMatchingFailure
     end
-  else extract_bound_aux (k + 1) accu frels stk
+  else extract_bound_aux (k + 1) accu frels ctx
 
-let extract_bound_vars frels stk =
-  extract_bound_aux 1 Id.Set.empty frels stk
+let extract_bound_vars frels ctx =
+  extract_bound_aux 1 Id.Set.empty frels ctx
 
 let dummy_constr = mkProp
 
@@ -134,20 +131,20 @@ let make_renaming ids = function
   end
 | _ -> dummy_constr
 
-let merge_binding allow_bound_rels stk n cT subst =
-  let c = match stk with
+let merge_binding allow_bound_rels ctx n cT subst =
+  let c = match ctx with
   | [] -> (* Optimization *)
     ([], cT)
   | _ ->
     let frels = free_rels cT in
     if allow_bound_rels then
-      let vars = extract_bound_vars frels stk in
+      let vars = extract_bound_vars frels ctx in
       let ordered_vars = Id.Set.elements vars in
       let rename binding = make_renaming ordered_vars binding in
-      let renaming = List.map rename stk in
+      let renaming = List.map rename ctx in
       (ordered_vars, substl renaming cT)
     else
-      let depth = List.length stk in
+      let depth = List.length ctx in
       let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
       if depth < min_elt then
         ([], lift (- depth) cT)
@@ -155,7 +152,8 @@ let merge_binding allow_bound_rels stk n cT subst =
   in
   constrain n c subst
       
-let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
+let matches_core env sigma convert allow_partial_app allow_bound_rels
+    (binding_vars,pat) c =
   let convref ref c = 
     match ref, kind_of_term c with
     | VarRef id, Var id' -> Names.id_eq id id'
@@ -168,7 +166,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	    is_conv env sigma c' c
        else false)
   in
-  let rec sorec stk env subst p t =
+  let rec sorec ctx env subst p t =
     let cT = strip_outer_cast t in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
@@ -181,11 +179,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
         let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
         let frels = free_rels cT in
         if Int.Set.subset frels relset then
-          constrain n ([], build_lambda relargs stk cT) subst
+          constrain n ([], build_lambda relargs ctx cT) subst
         else
           raise PatternMatchingFailure
 
-      | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
+      | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst
 
       | PMeta None, m -> subst
 
@@ -203,10 +201,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 
       | PSort (GType _), Sort (Type _) -> subst
 
-      | PApp (p, [||]), _ -> sorec stk env subst p t
+      | PApp (p, [||]), _ -> sorec ctx env subst p t
 
       | PApp (PApp (h, a1), a2), _ ->
-          sorec stk env subst (PApp(h,Array.append a1 a2)) t
+          sorec ctx env subst (PApp(h,Array.append a1 a2)) t
 
       | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
          (let diff = Array.length args2 - Array.length args1 in
@@ -216,13 +214,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
             let subst =
               match meta with
               | None -> subst
-              | Some n -> merge_binding allow_bound_rels stk n c subst in
-            Array.fold_left2 (sorec stk env) subst args1 args22
+              | Some n -> merge_binding allow_bound_rels ctx n c subst in
+            Array.fold_left2 (sorec ctx env) subst args1 args22
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
 	    | Proj (pr, c) when not (Projection.unfolded pr) ->
 	      (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
-		     sorec stk env subst p term
+		     sorec ctx env subst p term
 	       with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 	    | _ -> raise PatternMatchingFailure)
 	   
@@ -233,15 +231,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
 	  if Projection.equal pr1 pr then 
-	    try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2
+	    try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
 	    with Invalid_argument _ -> raise PatternMatchingFailure
 	  else raise PatternMatchingFailure
 	| _, Proj (pr,c) when not (Projection.unfolded pr) ->
 	  (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
-		 sorec stk env subst p term
+		 sorec ctx env subst p term
 	   with Retyping.RetypeError _ -> raise PatternMatchingFailure)	    
 	| _, _ ->
-          try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
+          try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
       | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
@@ -250,37 +248,37 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	
       | PApp (c, args), Proj (pr, c2) ->
 	(try let term = Retyping.expand_projection env sigma pr c2 [] in
-	       sorec stk env subst p term
+	       sorec ctx env subst p term
 	 with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
       | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
-          sorec stk env subst c1 c2
+          sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na1,na2,t2)::stk) (Environ.push_rel (na2,Some c2,t2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
-	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
-	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
-	  let n = rel_context_length ctx in
-          let n' = rel_context_length ctx' in
+	  let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
+	  let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
+	  let n = rel_context_length ctx_b2 in
+          let n' = rel_context_length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
-	    let s =
-	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
-	    let s' =
-	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
+            let f l (na,_,t) = (Anonymous,na,t)::l in
+	    let ctx_br = List.fold_left f ctx ctx_b2 in
+	    let ctx_br' = List.fold_left f ctx ctx_b2' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
-	    sorec s' (Environ.push_rel_context ctx' env)
-	      (sorec s (Environ.push_rel_context ctx env) (sorec stk env subst a1 a2) b1 b2) b1' b2'
+	    sorec ctx_br' (Environ.push_rel_context ctx_b2' env)
+	      (sorec ctx_br (Environ.push_rel_context ctx_b2 env)
+                 (sorec ctx env subst a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
 
@@ -301,9 +299,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	    (* (ind,j+1) is normally known to be a correct constructor
 	       and br2 a correct match over the same inductive *)
 	    assert (j < n2);
-	    sorec stk env subst c br2.(j)
+	    sorec ctx env subst c br2.(j)
 	  in
-	  let chk_head = sorec stk env (sorec stk env subst a1 a2) p1 p2 in
+	  let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
 	  List.fold_left chk_branch chk_head br1
 
       |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
@@ -319,7 +317,8 @@ let matches_core_closed env sigma convert allow_partial_app pat c =
 
 let extended_matches env sigma = matches_core env sigma false true true
 
-let matches env sigma pat c = snd (matches_core_closed env sigma false true pat c)
+let matches env sigma pat c =
+  snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
 
 let special_meta = (-1)
 
@@ -464,10 +463,10 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
 
-let match_subterm env sigma pat c = sub_match env sigma pat c
+let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c
 
 let match_appsubterm env sigma pat c = 
-  sub_match ~partial_app:true env sigma pat c
+  sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c
 
 let match_subterm_gen env sigma app pat c = 
   sub_match ~partial_app:app env sigma pat c
@@ -481,11 +480,12 @@ let is_matching_head env sigma pat c =
   with PatternMatchingFailure -> false
 
 let is_matching_appsubterm ?(closed=true) env sigma pat c =
+  let pat = (Id.Set.empty,pat) in
   let results = sub_match ~partial_app:true ~closed env sigma pat c in
   not (IStream.is_empty results)
 
-let matches_conv env sigma c p =
-  snd (matches_core_closed env sigma true false c p)
+let matches_conv env sigma p c =
+  snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
 
 let is_matching_conv env sigma pat n =
   try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 67854a893..b9dcb0af2 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -41,7 +41,8 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    variables or metavariables have the same name, the metavariable,
    or else the rightmost bound variable, takes precedence *)
 val extended_matches :
-  env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map
+  env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern ->
+  constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
@@ -72,8 +73,10 @@ val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_
 val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
 
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) ->
-   constr_pattern -> constr -> matching_result IStream.t
+val match_subterm_gen : env -> Evd.evar_map ->
+  bool (** true = with app context *) ->
+  Tacexpr.binding_bound_vars * constr_pattern -> constr ->
+  matching_result IStream.t
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a2189d5e4..754ad8f58 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -130,6 +130,8 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
 
 (* We retype applications to ensure the universe constraints are collected *)
 
+exception IllTypedInstance of env * types * types
+
 let recheck_applications conv_algo env evdref t =
   let rec aux env t =
     match kind_of_term t with
@@ -146,7 +148,7 @@ let recheck_applications conv_algo env evdref t =
 			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
 		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
-	 | _ -> assert false
+	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
      in aux 0 fty
     | _ ->
@@ -1134,8 +1136,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   else
     raise (CannotProject (evd,ev1'))
 
-exception IllTypedInstance of env * types * types
-
 let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 454d64f01..3a76e8bd7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Names
+open Nameops
 open Globnames
 open Misctypes
 open Glob_term
@@ -183,37 +184,32 @@ let map_glob_constr_left_to_right f = function
 
 let map_glob_constr = map_glob_constr_left_to_right
 
-let fold_glob_constr f acc =
-  let rec fold acc = function
+let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
+
+let fold_glob_constr f acc = function
   | GVar _ -> acc
-  | GApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | GApp (_,c,args) -> List.fold_left f (f acc c) args
   | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
-      fold (fold acc b) c
+    f (f acc b) c
   | GCases (_,_,rtntypopt,tml,pl) ->
-      List.fold_left fold_pattern
-	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
-	pl
-    | GLetTuple (_,_,rtntyp,b,c) ->
-	fold (fold (fold_return_type acc rtntyp) b) c
-    | GIf (_,c,rtntyp,b1,b2) ->
-	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
-    | GRec (_,_,_,bl,tyl,bv) ->
-	let acc = Array.fold_left
-	  (List.fold_left (fun acc (na,k,bbd,bty) ->
-	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
-	Array.fold_left fold (Array.fold_left fold acc tyl) bv
-    | GCast (_,c,k) ->
-        let r = match k with
-        | CastConv t | CastVM t | CastNative t -> fold acc t | CastCoerce -> acc
-        in
-        fold r c
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
-
-  and fold_pattern acc (_,idl,p,c) = fold acc c
-
-  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
-
-  in fold acc
+    let fold_pattern acc (_,idl,p,c) = f acc c in
+    List.fold_left fold_pattern
+      (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml))
+      pl
+  | GLetTuple (_,_,rtntyp,b,c) ->
+    f (f (fold_return_type f acc rtntyp) b) c
+  | GIf (_,c,rtntyp,b1,b2) ->
+    f (f (f (fold_return_type f acc rtntyp) c) b1) b2
+  | GRec (_,_,_,bl,tyl,bv) ->
+    let acc = Array.fold_left
+      (List.fold_left (fun acc (na,k,bbd,bty) ->
+	f (Option.fold_left f acc bbd) bty)) acc bl in
+    Array.fold_left f (Array.fold_left f acc tyl) bv
+  | GCast (_,c,k) ->
+    let acc = match k with
+      | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
+    f acc c
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
@@ -328,6 +324,65 @@ let free_glob_vars  =
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
+let add_and_check_ident id set =
+  if Id.Set.mem id set then
+    Pp.(msg_warning
+      (str "Collision between bound variables of name " ++ Id.print id));
+  Id.Set.add id set
+
+let bound_glob_vars =
+  let rec vars bound = function
+    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c ->
+        let bound = name_fold add_and_check_ident na bound in
+        fold_glob_constr vars bound c
+    | GCases (loc,sty,rtntypopt,tml,pl) ->
+	let bound = vars_option bound rtntypopt in
+	let bound =
+          List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
+	List.fold_left vars_pattern bound pl
+    | GLetTuple (loc,nal,rtntyp,b,c) ->
+	let bound = vars_return_type bound rtntyp in
+	let bound = vars bound b in
+	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
+	vars bound c
+    | GIf (loc,c,rtntyp,b1,b2) ->
+	let bound = vars_return_type bound rtntyp in
+	let bound = vars bound c in
+	let bound = vars bound b1 in
+	vars bound b2
+    | GRec (loc,fk,idl,bl,tyl,bv) ->
+	let bound = Array.fold_right Id.Set.add idl bound in
+	let vars_fix i bound fid =
+	  let bound =
+	    List.fold_left
+	      (fun bound (na,k,bbd,bty) ->
+		 let bound = vars_option bound bbd in
+		 let bound = vars bound bty in
+		 name_fold add_and_check_ident na bound
+	      )
+	      bound
+	      bl.(i)
+	  in
+	  let bound = vars bound tyl.(i) in
+	  vars bound bv.(i)
+	in
+	Array.fold_left_i vars_fix bound idl
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
+    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
+
+  and vars_pattern bound (loc,idl,p,c) =
+    let bound = List.fold_right add_and_check_ident idl bound in
+    vars bound c
+
+  and vars_option bound = function None -> bound | Some p -> vars bound p
+
+  and vars_return_type bound (na,tyopt) =
+    let bound = name_fold add_and_check_ident na bound in
+    vars_option bound tyopt
+  in
+  fun rt ->
+    vars Id.Set.empty rt
+
 (** Mapping of names in binders *)
 
 (* spiwack: I used a smartmap-style kind of mapping here, because the
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index e514fd529..25746323f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -38,6 +38,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
+val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 17eafb19e..bb21b87d3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -322,8 +322,8 @@ let ltac_interp_name_env k0 lvar env =
   push_rel_context ctxt env
 
 let invert_ltac_bound_name lvar env id0 id =
-  let id = Id.Map.find id lvar.ltac_idents in
-  try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+  let id' = Id.Map.find id lvar.ltac_idents in
+  try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
     errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 937ad2b9d..6bd65d0a2 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -76,25 +76,6 @@ let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
 let coq_all = find_global ["Init"; "Logic"] "all"
 let impl = find_global ["Program"; "Basics"] "impl"
 
-(* let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip") *)
-
-(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) *)
-
-(* let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation") *)
-(* let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") *)
-(* let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") *)
-(* let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") *)
-(* let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation") *)
-(* let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation") *)
-(* let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation") *)
-(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-(* let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) *)
-
-(* let proper_type = lazy (Universes.constr_of_global (Lazy.force proper_class).cl_impl) *)
-(* let proper_proxy_type = lazy (Universes.constr_of_global (Lazy.force proper_proxy_class).cl_impl) *)
-
-
-
 (** Bookkeeping which evars are constraints so that we can 
     remove them at the end of the tactic. *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 593e46b05..96d0b592b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1038,11 +1038,12 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt
 (* Reads a pattern by substituting vars of lfun *)
 let use_types = false
 
-let eval_pattern lfun ist env sigma (_,pat as c) =
+let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
+  let bound_names = bound_glob_vars glob in
   if use_types then
-    pi3 (interp_typed_pattern ist env sigma c)
+    (bound_names,pi3 (interp_typed_pattern ist env sigma c))
   else
-    instantiate_pattern env sigma lfun pat
+    (bound_names,instantiate_pattern env sigma lfun pat)
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index abeb47c3b..d8e6dd0ae 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -32,7 +32,7 @@ val match_term :
   Environ.env ->
   Evd.evar_map ->
   Term.constr ->
-  (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
 
 (** [match_goal env sigma hyps concl rules] matches the goal
@@ -45,5 +45,5 @@ val match_goal:
   Evd.evar_map ->
   Context.named_context ->
   Term.constr ->
-  (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b5dc2dc8b..27166bf48 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -739,12 +739,11 @@ let reduction_clause redexp cl =
 let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
+  let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   let tac = tclMAP (fun (where,redexp) ->
-    e_reduct_option ~check:true
+    e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
-  match redexp with
-  | Fold _ | Pattern _ -> with_check tac goal
-  | _ -> tac goal
+  if check then with_check tac goal else tac goal
 
 (* Unfolding occurrences of a constant *)
 
diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
new file mode 100644
index 000000000..6a5e9a402
--- /dev/null
+++ b/test-suite/bugs/closed/4366.v
@@ -0,0 +1,15 @@
+Fixpoint stupid (n : nat) : unit :=
+match n with
+| 0 => tt
+| S n =>
+  let () := stupid n in
+  let () := stupid n in
+  tt
+end.
+
+Goal True.
+Proof.
+pose (v := stupid 24).
+Timeout 2 vm_compute in v.
+exact I.
+Qed.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 000000000..d003c70df
--- /dev/null
+++ b/test-suite/output/ltac.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
new file mode 100644
index 000000000..7e2610c7d
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,17 @@
+(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
+Goal True.
+Fail let T := constr:((fun a b : nat => a+b) 1 1) in
+  lazymatch T with
+  | (fun x z => ?y) 1 1
+    => pose ((fun x _ => y) 1 1)
+  end.
+Abort.
+
+(* This should not raise a warning (see #4317) *)
+Goal True.
+assert (H:= eq_refl ((fun x => x) 1)).
+let HT := type of H in
+lazymatch goal with
+| H1 : HT |- _ => idtac
+end.
+Abort.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index f9df021dc..6c4d4ae98 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -306,3 +306,14 @@ let x := ipattern:y in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.
+
+(* An example suggested by Jason (see #4317) showing the intended semantics *)
+(* Order of binders is reverted because y is just told to depend on x *)
+
+Goal 1=1.
+let T := constr:(fun a b : nat => a) in
+  lazymatch T with
+  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
+  end.
+exact (eq_refl n).
+Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e54a82c19..7c86d2d05 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -41,13 +41,13 @@ open Vernacexpr
 let do_universe l = Declare.do_universe l  
 let do_constraint l = Declare.do_constraint l
 
-let rec under_binders env f n c =
-  if Int.equal n 0 then snd (f env Evd.empty c) else
+let rec under_binders env sigma f n c =
+  if Int.equal n 0 then snd (f env sigma c) else
     match kind_of_term c with
       | Lambda (x,t,c) ->
-	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
+	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) sigma f (n-1) c)
       | LetIn (x,b,t,c) ->
-	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
+	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) sigma f (n-1) c)
       | _ -> assert false
 
 let rec complete_conclusion a cs = function
@@ -67,14 +67,14 @@ let rec complete_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
-let red_constant_entry n ce = function
+let red_constant_entry n ce sigma = function
   | None -> ce
   | Some red ->
       let proof_out = ce.const_entry_body in
       let env = Global.env () in
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun ((body,ctx),eff) ->
-          (under_binders env
+          (under_binders env sigma
              (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
 
 let interp_definition pl bl p red_option c ctypopt =
@@ -125,7 +125,7 @@ let interp_definition pl bl p red_option c ctypopt =
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
-  red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
+  red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, imps
 
 let check_definition (ce, evd, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);