diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 16:09:11 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:10:16 +0000 |
| commit | d3127693d4a2125088aa512f593d782843482f2a (patch) | |
| tree | f96a8b0d0efd46ab223dc0d360ea7a48302dea0b /vernac/ppvernac.ml | |
| parent | 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 (diff) | |
[vernac] use plain strings as attribute names
The concrete syntax is still restricted to identifiers.
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 024c145aa..e5547d9b7 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1194,7 +1194,7 @@ open Pputils return (str "}") let rec pr_vernac_flag (k, v) = - let k = keyword (Names.Id.to_string k) in + let k = keyword k in match v with | VernacFlagEmpty -> k | VernacFlagLeaf v -> k ++ str " = " ++ qs v |