aboutsummaryrefslogtreecommitdiff
path: root/vernac/ppvernac.ml
diff options
context:
space:
mode:
authorSimonBoulier2018-11-05 11:45:47 +0100
committerSimonBoulier2019-08-16 11:43:51 +0200
commit33f7877dc675cd1c2ce5ffd8da04e65b4d029676 (patch)
treea59cd301dd693382aba593825309a7e214ea21f0 /vernac/ppvernac.ml
parentbc4560fa6c88aadcb2ee8312a950a7ce17fc33ee (diff)
Add [Print Typing Flags] command.
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 ->