Merge PR #6128: Simplification: cumulativity information is variance information.

4 files changed, 15 insertions, 6 deletions

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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a79..35487e09c 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -113,13 +113,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
 let instantiate_cumulativity_info cumi =
   let open Univ in
   let univs = ACumulativityInfo.univ_context cumi in
-  let subtyp = ACumulativityInfo.subtyp_context cumi in
   let expose ctx =
     let inst = AUContext.instance ctx in
     let cst = AUContext.instantiate inst ctx in
     UContext.make (inst, cst)
   in
-  CumulativityInfo.make (expose univs, expose subtyp)
+  CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
 
 let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))