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`

---
 library/assumptions.ml  | 12 ++++++++++--
 library/assumptions.mli |  1 +
 printing/printer.ml     |  2 ++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/library/assumptions.ml b/library/assumptions.ml
index b2363bce61..4635278202 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -26,6 +26,7 @@ open Globnames
 type axiom =
   | Constant of constant (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom      (* An assumed fact. *)
@@ -43,7 +44,10 @@ struct
         con_ord k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
-    | Positive _ , Constant _ -> 1
+    | Guarded k1 , Guarded k2 ->
+        con_ord k1 k2
+    | _ , Constant _ -> 1
+    | _ , Positive _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -221,7 +225,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
     if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
     else accu
   | ConstRef kn ->
-    let cb = lookup_constant kn in
+      let cb = lookup_constant kn in
+      let accu =
+        if cb.const_checked_guarded then accu
+        else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu
+      in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Axiom (Constant kn)) t accu
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 72ed6acf0d..499e2b42e4 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -16,6 +16,7 @@ open Globnames
 type axiom =
   | Constant of constant (** An axiom or a constant. *)
   | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *)
+  | Guarded of constant (** A constant whose (co)fixpoints have been assumed to be guarded *)
 type context_object =
   | Variable of Id.t  (** A section variable or a Let definition. *)
   | Axiom of axiom       (** An assumed fact. *)
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