aboutsummaryrefslogtreecommitdiff
path: root/vernac/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/ppvernac.ml')
-rw-r--r--vernac/ppvernac.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0eb0b1b6f6..873a119e39 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -514,6 +514,8 @@ let string_of_theorem_kind = let open Decls in function
++ pr_class_rawexpr t
| PrintCanonicalConversions ->
keyword "Print Canonical Structures"
+ | PrintTypingFlags ->
+ keyword "Print Typing Flags"
| PrintTables ->
keyword "Print Tables"
| PrintHintGoal ->