From 0c94de1f8c598c1869f71fee86bdbe4f0000a502 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 4 May 2017 19:12:45 +0200
Subject: Add printing of cumulativity in inductive types

---
 printing/ppvernac.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6a47c308d3..4a5cfe6301 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -759,8 +759,10 @@ open Decl_kinds
                        | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
                        | Class _ -> "Class" | Variant -> "Variant"
           in
-          let cm = if cum then "Cumulative" else "NonCumulative" in
-          cm ^ " " ^ kind
+          if p then
+            let cm = if cum then "Cumulative" else "NonCumulative" in
+            cm ^ " " ^ kind
+          else kind
         in
         return (
           hov 1 (pr_oneind key (List.hd l)) ++
-- 
cgit v1.2.3