aboutsummaryrefslogtreecommitdiff
path: root/vernac/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/ppvernac.ml')
-rw-r--r--vernac/ppvernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1742027076..a1bd99c237 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function
keyword "Print Coercion Paths" ++ spc()
++ pr_class_rawexpr s ++ spc()
++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
+ | PrintCanonicalConversions qids ->
+ keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
| PrintTypingFlags ->
keyword "Print Typing Flags"
| PrintTables ->