From 476189527703aaf9caf5612e8395ce3b8ddb088f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Jun 2015 16:10:29 +0200
Subject: Make inductives that were assumed positive appear in `Print
 Assumptions`.

They appear as axioms of the form `Foo is positive`.
---
 printing/printer.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 6525428254..b57fa90797 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -729,14 +729,21 @@ let pr_assumptionset env s =
       try str " : " ++ pr_ltype typ
       with e when Errors.noncritical e -> mt ()
     in
+    let pr_axiom env ax typ =
+      match ax with
+      | Constant kn ->
+          safe_pr_constant env kn ++ safe_pr_ltype typ
+      | Positive m ->
+          hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+    in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
         let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
         (var :: v, a, o, tr)
-      | Axiom kn ->
-        let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
+      | Axiom axiom ->
+        let ax = pr_axiom env axiom typ in
         (v, ax :: a, o, tr)
       | Opaque kn ->
         let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
-- 
cgit v1.2.3


From 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 15:11:01 +0200
Subject: Show assumptions of well-foundedness in `Print Assumptions`

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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index b57fa90797..8609b19c9a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -735,6 +735,8 @@ let pr_assumptionset env s =
           safe_pr_constant env kn ++ safe_pr_ltype typ
       | Positive m ->
           hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+      | Guarded kn ->
+          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
-- 
cgit v1.2.3