From 33f7877dc675cd1c2ce5ffd8da04e65b4d029676 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 5 Nov 2018 11:45:47 +0100
Subject: Add [Print Typing Flags] command.

---
 printing/printer.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'printing/printer.ml')

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
-- 
cgit v1.2.3