diff options
| author | SimonBoulier | 2018-11-05 11:45:47 +0100 |
|---|---|---|
| committer | SimonBoulier | 2019-08-16 11:43:51 +0200 |
| commit | 33f7877dc675cd1c2ce5ffd8da04e65b4d029676 (patch) | |
| tree | a59cd301dd693382aba593825309a7e214ea21f0 /vernac | |
| parent | bc4560fa6c88aadcb2ee8312a950a7ce17fc33ee (diff) | |
Add [Print Typing Flags] command.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 1 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
4 files changed, 5 insertions, 0 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dcd1979a85..fdf43196b0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1035,6 +1035,7 @@ GRAMMAR EXTEND Gram | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } | IDENT "Hint" -> { PrintHintGoal } 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 -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc51dd46f3..4fb0129236 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1928,6 +1928,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function + | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () | PrintFullContext-> print_full_context_typ env sigma | PrintSectionContext qid -> print_sec_context_typ env sigma qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 0968632c2d..c15baf6157 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -24,6 +24,7 @@ type goal_reference = | GoalId of Id.t type printable = + | PrintTypingFlags | PrintTables | PrintFullContext | PrintSectionContext of qualid |