From a9240de59f6822f55a57d0e6453bd0635795720d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 11 Nov 2017 22:02:20 +0100
Subject: Print inductive cumulativity info in About.

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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index a63004cebe..d720bc2f8c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -263,10 +263,10 @@ let pr_universe_ctx_set sigma c =
   else
     mt()
 
-let pr_universe_ctx sigma c =
+let pr_universe_ctx sigma ?variance c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
+      (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
   else
     mt()
 
-- 
cgit v1.2.3