From 3c2044f06ba4a293c6d0f19fdfdbdbd253e228c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Sep 2020 10:12:25 -0700 Subject: [PATCH] chore: add coercion for new frontend --- src/Lean/Parser/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index efa1d81354..56f11f7255 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1218,8 +1218,8 @@ fun c s => def unquotedSymbol : Parser := { fn := unquotedSymbolFn } -instance stringToParserCoe : HasCoe String Parser := -⟨fun s => symbol s ⟩ +instance stringToParserCoeOld : HasCoe String Parser := ⟨fun s => symbol s ⟩ +instance stringToParserCoe : Coe String Parser := ⟨fun s => symbol s ⟩ namespace ParserState