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