From 1aa398415cfc944877a2b1925a848fcd20ff44ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Dec 2019 14:38:59 -0800
Subject: [PATCH] fix: accidental variable shadowing

---
 src/Init/Lean/Meta/ExprDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 9c91b16a5c..60e4f8917b 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -29,7 +29,7 @@ if a.isLambda && !b.isLambda then do
   bType ← inferType b;
   bType ← whnfUsingDefault bType;
   match bType with
-  | Expr.forallE n d b c =>
+  | Expr.forallE n d _ c =>
     let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
     try $ isExprDefEqAux a b'
   | _ => pure false