diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 56dfaa54a..5fbe1f4e4 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -210,7 +210,10 @@ open Pputils | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_qualid l + ++ (match l with + | HintsVariables -> keyword "Variables" + | HintsConstants -> keyword "Constants" + | HintsReferences l -> prlist_with_sep sep pr_qualid l) | HintsMode (m, l) -> keyword "Mode" ++ spc () |