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

---
 printing/prettyp.ml  | 11 ++++++++++-
 printing/printer.ml  |  4 ++--
 printing/printer.mli |  3 ++-
 3 files changed, 14 insertions(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b7886d11..114a071ee 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,15 @@ let print_ref reduce ref udecl =
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let variance = match ref with
+    | VarRef _ | ConstRef _ -> None
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+      let mind = Environ.lookup_mind ind (Global.env ()) in
+      begin match mind.Declarations.mind_universes with
+        | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
+        | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
+      end
+  in
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
@@ -89,7 +98,7 @@ let print_ref reduce ref udecl =
     else mt ()
   in
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-  	   Printer.pr_universe_ctx sigma univs)
+           Printer.pr_universe_ctx sigma ?variance univs)
 
 (********************************)
 (** Printing implicit arguments *)
diff --git a/printing/printer.ml b/printing/printer.ml
index a63004ceb..d720bc2f8 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()
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 804014745..a3427920a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,8 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
-val pr_universe_ctx        : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.UContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
 val pr_constant_universes  : evar_map -> Entries.constant_universes_entry -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
-- 
cgit v1.2.3