From cd440dbd43a632cf8f445a80d034f36e4235c63e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 10 Oct 2015 13:02:56 +0200
Subject: Fix a few latex errors in documentation of Proof Using (e.g. \tt*).

---
 doc/refman/RefMan-pro.tex | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 5dbf315535..481afa8f87 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.
-- 
cgit v1.2.3


From d399671f3f1a667a47540071feecb20baf115418 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 11:21:23 +0200
Subject: Constr_matching: renaming misleading name stk into ctx.

---
 pretyping/constr_matching.ml | 92 ++++++++++++++++++++++----------------------
 1 file changed, 46 insertions(+), 46 deletions(-)

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a0493777a5..585be9c720 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -80,21 +80,21 @@ let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
     (names, terms)
 | _ -> subst
 
-let rec build_lambda vars stk m = match vars with
+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 +108,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 +134,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)
@@ -168,7 +168,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 +181,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 +203,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 +216,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 +233,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 +250,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 (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 (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 (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 +301,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
-- 
cgit v1.2.3


From 2e07ecfce221840047b2f95c93acdb79a4fe0985 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 13:42:11 +0200
Subject: Fixing obviously untested fold_glob_constr and iter_glob_constr.

---
 pretyping/glob_ops.ml | 51 +++++++++++++++++++++++----------------------------
 1 file changed, 23 insertions(+), 28 deletions(-)

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 454d64f01b..5b02c8cd15 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -183,37 +183,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) ()
 
-- 
cgit v1.2.3


From ae5305a4837cce3c7fd61b92ce8110ac66ec2750 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 15:05:10 +0200
Subject: Refining 0c320e79ba30 in fixing interpretation of constr under
 binders which was broken after it became possible to have binding names
 themselves bound to ltac variables (2fcc458af16b).

Interpretation was corrected, but error message was damaged.
---
 pretyping/pretyping.ml     |  4 ++--
 test-suite/output/ltac.out |  2 ++
 test-suite/output/ltac.v   |  8 ++++++++
 test-suite/success/ltac.v  | 11 +++++++++++
 4 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/output/ltac.out
 create mode 100644 test-suite/output/ltac.v

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6306739b7a..746b4000ee 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/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 0000000000..d003c70df9
--- /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 0000000000..567e21edbe
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,8 @@
+(* 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.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index f9df021dc2..6c4d4ae98f 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.
-- 
cgit v1.2.3


From e9995f6e9f9523d4738d9ee494703b6f96bf995d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 14:36:29 +0200
Subject: Fixing untimely unexpected warning "Collision between bound
 variables" (#4317).

Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
---
 intf/tacexpr.mli              |  5 ++--
 pretyping/constr_matching.ml  | 46 ++++++++++++++++-----------------
 pretyping/constr_matching.mli |  9 ++++---
 pretyping/glob_ops.ml         | 60 +++++++++++++++++++++++++++++++++++++++++++
 pretyping/glob_ops.mli        |  1 +
 tactics/tacinterp.ml          |  7 ++---
 tactics/tactic_matching.mli   |  4 +--
 test-suite/output/ltac.v      |  9 +++++++
 8 files changed, 108 insertions(+), 33 deletions(-)

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 2b37c580ea..eb4e5ae7d3 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -114,6 +114,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 =
@@ -325,7 +326,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
@@ -386,7 +387,7 @@ type raw_tactic_arg =
 
 type t_trm = Term.constr
 type t_utrm = Glob_term.closed_glob_constr
-type t_pat = glob_constr_and_expr * constr_pattern
+type t_pat = glob_constr_pattern_and_expr
 type t_cst = evaluable_global_reference and_short_name
 type t_ref = ltac_constant located
 type t_nam  = Id.t
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 585be9c720..19c85c9e27 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,16 +65,17 @@ 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 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
 | [] ->
@@ -155,7 +152,8 @@ let merge_binding allow_bound_rels ctx 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'
@@ -258,15 +256,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
 	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+            (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)::ctx) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+            (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)::ctx) (Environ.push_rel (na2,Some c2,t2) env)
-            (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2
+            (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,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
@@ -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 67854a893d..b9dcb0af26 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/glob_ops.ml b/pretyping/glob_ops.ml
index 5b02c8cd15..3a76e8bd74 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
@@ -323,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 e514fd529e..25746323fb 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/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 593e46b05c..96d0b592b8 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 abeb47c3b9..d8e6dd0ae3 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/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 567e21edbe..9a60afe5f6 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -6,3 +6,12 @@ Fail let T := constr:((fun a b : nat => a+b) 1 1) in
     => 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 "matched"
+end.
+Abort.
-- 
cgit v1.2.3


From bf39345125d66d3efd9f934be91200013f57841c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 16:29:54 +0200
Subject: Documenting matching under binders.

---
 doc/refman/RefMan-ltac.tex | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d388840df5..04c356e44f 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
-- 
cgit v1.2.3


From cd9a2e9e59d87801790859ddd26d225d71be7f7c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 17:26:30 +0200
Subject: Fixing test-suite

---
 test-suite/output/ltac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 9a60afe5f6..7e2610c7d7 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -12,6 +12,6 @@ Goal True.
 assert (H:= eq_refl ((fun x => x) 1)).
 let HT := type of H in
 lazymatch goal with
-| H1 : HT |- _ => idtac "matched"
+| H1 : HT |- _ => idtac
 end.
 Abort.
-- 
cgit v1.2.3


From f8658b06b98e59e7f6397c6082e4b9b399499948 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2015 18:48:01 +0200
Subject: Fixing bug #4366: Conversion tactics recheck uselessly
 convertibility.

---
 tactics/tactics.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b113ed31e9..0d6a26a113 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -726,12 +726,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 *)
 
-- 
cgit v1.2.3


From 303694c6436b36b114f4919ad7cacc9c053d11a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2015 19:06:26 +0200
Subject: Adding test for bug #4366.

---
 test-suite/bugs/closed/4366.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/4366.v

diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
new file mode 100644
index 0000000000..6a5e9a4023
--- /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.
-- 
cgit v1.2.3


From c1ebc07204c65b4570333748b63a3ef60618b026 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Oct 2015 10:51:08 +0200
Subject: Gather VM tags in Cbytecodes.

---
 kernel/cbytecodes.ml  | 11 +++++++----
 kernel/cbytecodes.mli | 10 ++++++----
 kernel/vm.ml          |  8 --------
 3 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 891d95378b..448bf85444 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 8f594a45b5..03d6383057 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/vm.ml b/kernel/vm.ml
index 29e2ee601d..eacd803fd4 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 ***)
 (*******************************************)
-- 
cgit v1.2.3


From a479aa6e8dbd1dda1af2412f8c1e1ff40f0d5a0b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Oct 2015 12:57:23 +0200
Subject: Fix rechecking of applications: it can be given ill-typed terms.
 Fixes math-classes.

---
 pretyping/evarsolve.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a2189d5e4f..754ad8f588 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
-- 
cgit v1.2.3


From b9a3925288af0cf3023c9a0073dc1eb295270de8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Oct 2015 13:12:26 +0200
Subject: Fix Definition id := Eval <redexpr> in by passing the right universe
 context to the reduction function. Fixes MapleMode.

---
 toplevel/command.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index e54a82c19b..7c86d2d059 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);
-- 
cgit v1.2.3


From 50183ce7200d6059b4146c0cc4933aa524178c02 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Oct 2015 15:39:20 +0200
Subject: Univs: be more restrictive for template polymorphic constants: only
 direct aliases are ok, and indices should not be made polymorphic. Fixes
 NFix.

---
 kernel/inductive.ml |  5 +----
 kernel/typeops.ml   | 14 ++++++++++----
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a02d5e2055..1f8706652f 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 fe82d85d5d..8895bae5da 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
 
-- 
cgit v1.2.3


From 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Oct 2015 16:34:33 +0200
Subject: Remove code that was already commented out.

---
 tactics/rewrite.ml | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 937ad2b9d4..6bd65d0a21 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. *)
 
-- 
cgit v1.2.3