From 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
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')

diff --git a/printing/printer.ml b/printing/printer.ml
index b57fa9079..8609b19c9 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