From 941ad84ecef1ee2cf1f70af0eb4659ebce83846a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 12:44:36 -0700
Subject: [PATCH] fix: `getMkMatcherInputInContext`

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

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 40c2c5f0f5..f5129192e8 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -890,7 +890,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
       fvarDecls := localDecls.toList
       patterns := patterns.toList : Match.AltLHS }
 
-  return { matcherName, matchType, discrInfos := mkArray matcherApp.discrs.size {}, lhss }
+  return { matcherName, matchType, discrInfos := matcherInfo.discrInfos, lhss }
 
 
 def withMkMatcherInput