Add [Print Typing Flags] command.

6 files changed, 12 insertions, 0 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index ec1b9b8e49..9c74d8cfbb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1003,3 +1003,8 @@ let print_and_diff oldp newp =
         pr_open_subgoals ~proof
     in
     Feedback.msg_notice output;;
+
+let pr_typing_flags flags =
+  str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
+  ++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
+  ++ str "check_universes: " ++ bool flags.check_universes
diff --git a/printing/printer.mli b/printing/printer.mli
index a72f319636..0855f2d109 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -207,3 +207,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
+
+val pr_typing_flags : Declarations.typing_flags -> Pp.t
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