fix: Don't include syntax information in elaboration of math elements

This avoids spurious infoview display of the internal elaborated
constant type.

This bug is only observable after applying the fix in leanprover#700 ; will wait
for leanprover#700 and leanprover#699 to merge this so we can properly provide a test.

Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

Author: ejgallego

src/verso/Verso/Doc/Elab.lean

@@ -194,13 +194,13 @@ public meta def _root_.Lean.Doc.Syntax.code.expand : InlineExpander
 @[inline_expander Lean.Doc.Syntax.inline_math]
 public meta def _root_.Lean.Doc.Syntax.inline_math.expand : InlineExpander
   |  `(inline| \math code( $s )) =>
-    ``(Inline.math MathMode.inline $s)
+    ``(Inline.math MathMode.inline $(quote s.getString))
   | _ => throwUnsupportedSyntax
 
 @[inline_expander Lean.Doc.Syntax.display_math]
 public meta def _root_.Lean.Doc.Syntax.display_math.expand : InlineExpander
   |  `(inline| \displaymath code( $s )) =>
-    ``(Inline.math MathMode.display $s)
+    ``(Inline.math MathMode.display $(quote s.getString))
   | _ => throwUnsupportedSyntax