From 95ea0b92ea1ffefa2427bbf25507916cfec6d4dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 12:40:32 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/depElim1.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index 1c91efbe17..a01fc2f43b 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -154,7 +154,7 @@ def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp
 generalizeTelescope majors.toArray fun majors => do
   let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat
   let matchType ← mkForallFVars majors resultType
-  Match.mkMatcher { matcherName := elimName, matchType, numDiscrs := majors.size, lhss }
+  Match.mkMatcher { matcherName := elimName, matchType, discrInfos := mkArray majors.size {}, lhss }
 
 def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
 withDepElimFrom ex numPats fun majors alts => do