From 0c766b2e3b54d96713a79e40661653c5486822a8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 01:23:26 +0200
Subject: Print Assumptions shows engagement.

Seems to be morally required since we have the -type-in-type flag.
---
 printing/printer.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 33b95c2f56..18e4902255 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -742,7 +742,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
-  if ContextObjectMap.is_empty s then
+  if ContextObjectMap.is_empty s &&
+       engagement env = (PredicativeSet, StratifiedType) then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
@@ -788,6 +789,16 @@ let pr_assumptionset env s =
     let (vars, axioms, opaque, trans) = 
       ContextObjectMap.fold fold s ([], [], [], [])
     in
+    let theory =
+      if is_impredicative_set env then
+	[str "Set is impredicative"]
+      else []
+    in
+    let theory =
+      if type_in_type env then
+	str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+      else theory
+    in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -801,6 +812,7 @@ let pr_assumptionset env s =
       opt_list (str "Section Variables:") vars;
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
+      opt_list (str "Theory:") theory;
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-- 
cgit v1.2.3