From a806b1d47273b008507aa08a99e5e45fbfe5243b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 8 Oct 2014 17:17:02 +0200
Subject: Fix bug due to shadowing a variable name in tacred

---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bddd274ef..6fa785ed7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -915,7 +915,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
     | Some c ->
       (match kind_of_term (strip_lam c) with
       | CoFix _ | Fix _ -> s'
-      | Proj (p,c) when
+      | Proj (p,t) when
 	  (match kind_of_term constr with
 	  | Const (c', _) -> eq_constant (Projection.constant p) c'
 	  | _ -> false) ->
-- 
cgit v1.2.3