From 3e77c7cdef29296c8f94ac4d39026e0113613ea7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Dec 2020 16:09:24 +0100 Subject: [PATCH] fix: error position --- src/Lean/Elab/Do.lean | 2 +- tests/lean/match1.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 1583cd1b76..eb94f90d27 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -216,7 +216,7 @@ def hasBreakContinueReturn (c : Code) : Bool := | Code.«return» _ _ => true | _ => false -def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withFreshMacroScope do +def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withRef e <| withFreshMacroScope do let y ← `(y) let yName := y.getId let doElem ← `(doElem| let y ← $e:term) diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index 89a5352b4c..4617fcb36e 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -19,7 +19,7 @@ match1.lean:113:0: error: dependent match elimination failed, inaccessible patte .(j + j) constructor expected [false, true, true] -match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables +match1.lean:124:7: error: invalid match-expression, type of pattern variable 'a' contains metavariables ?m fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m fun (x : Nat × Nat) =>