diff options
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 |