Merge PR#613: Cumulativity for inductive types

1 files changed, 13 insertions, 0 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index d6f0778f75..3b0b6d5d23 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,6 +261,14 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_cumulativity_info sigma cumi =
+  if !Detyping.print_universes 
+  && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
+    fnl()++pr_in_comment (fun uii -> v 0 
+      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+  else
+    mt()
+
 (**********************************************************************)
 (* Global references *)
 
@@ -991,6 +999,11 @@ let pr_assumptionset env s =
 let xor a b = 
   (a && not b) || (not a && b)
 
+let pr_cumulative poly cum =
+  if poly then
+    if cum then str "Cumulative " else str "NonCumulative "
+  else mt ()
+
 let pr_polymorphic b = 
   let print = xor (Flags.is_universe_polymorphism ()) b in
   if print then