Make inductives that were assumed positive appear in `Print Assumptions`.

They appear as axioms of the form `Foo is positive`.

3 files changed, 36 insertions, 8 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 62645b2365..b2363bce61 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -23,9 +23,12 @@ open Declarations
 open Mod_subst
 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. *)
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant      (* An axiom or a constant. *)
+  | Axiom of axiom      (* An assumed fact. *)
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
 
@@ -33,10 +36,20 @@ type context_object =
 module OrderedContextObject =
 struct
   type t = context_object
+
+  let compare_axiom x y =
+    match x,y with
+    | Constant k1 , Constant k2 ->
+        con_ord k1 k2
+    | Positive m1 , Positive m2 ->
+        MutInd.CanOrd.compare m1 m2
+    | Positive _ , Constant _ -> 1
+    | _ -> -1
+
   let compare x y =
       match x , y with
       | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom k1 , Axiom k2 -> con_ord k1 k2
+      | Axiom a1 , Axiom a2 -> compare_axiom a1 a2
       | Opaque k1 , Opaque k2 -> con_ord k1 k2
       | Transparent k1 , Transparent k2 -> con_ord k1 k2
       | Axiom _ , Variable _ -> 1
@@ -211,7 +224,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
     let cb = lookup_constant kn in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
-      ContextObjectMap.add (Axiom kn) t accu
+      ContextObjectMap.add (Axiom (Constant kn)) t accu
     else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Opaque kn) t accu
@@ -220,6 +233,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
       ContextObjectMap.add (Transparent kn) t accu
     else
       accu
-  | IndRef _ | ConstructRef _ -> accu
+  | IndRef (m,_) | ConstructRef ((m,_),_) ->
+      let mind = Global.lookup_mind m in
+      if mind.mind_checked_positive then
+        accu
+      else
+        ContextObjectMap.add (Axiom (Positive m)) Constr.mkProp accu
   in
   Refmap.fold fold graph ContextObjectMap.empty
diff --git a/library/assumptions.mli b/library/assumptions.mli
index bb36a97259..72ed6acf0d 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -13,9 +13,12 @@ open Globnames
 
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
+type axiom =
+  | Constant of constant (** An axiom or a constant. *)
+  | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *)
 type context_object =
-  | Variable of Id.t  (** A section variable or a Let definition *)
-  | Axiom of constant       (** An axiom or a constant. *)
+  | Variable of Id.t  (** A section variable or a Let definition. *)
+  | Axiom of axiom       (** An assumed fact. *)
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
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