From bd89bdde8afe08fb03e10d771aef7cf9ae660ded Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Feb 2022 11:17:39 -0800
Subject: [PATCH] fix: core library

see #1018
---
 src/Init/Data/Array/InsertionSort.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Array/InsertionSort.lean b/src/Init/Data/Array/InsertionSort.lean
index 0f8a76610b..f1b17e590c 100644
--- a/src/Init/Data/Array/InsertionSort.lean
+++ b/src/Init/Data/Array/InsertionSort.lean
@@ -18,7 +18,7 @@ where
       else
         a
   @[specialize] swapLoop (a : Array α) (j : Nat) (h : j < a.size) : Array α :=
-    match he:j with
+    match (generalizing := false) he:j with -- using `generalizing` because we don't want to refine the type of `h`
     | 0    => a
     | j'+1 =>
       have h' : j' < a.size := by subst j; exact Nat.lt_trans (Nat.lt_succ_self _) h