Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

4 files changed, 19 insertions, 42 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e0403a9f97..797b6faa08 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -86,10 +86,7 @@ let print_ref reduce ref udecl =
     | VarRef _ | ConstRef _ -> None
     | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
       let mind = Environ.lookup_mind ind 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
+      mind.Declarations.mind_variance
   in
   let inst =
     if Global.is_polymorphic ref
@@ -98,7 +95,7 @@ let print_ref reduce ref udecl =
   in
   let priv = None in (* We deliberately don't print private univs in About. *)
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
+         Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -562,11 +559,11 @@ let print_constant with_values sep sp udecl =
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
-      | Monomorphic_const ctx ->
-        Monomorphic_const (ContextSet.union body_uctxs ctx)
-      | Polymorphic_const ctx ->
+      | Monomorphic ctx ->
+        Monomorphic (ContextSet.union body_uctxs ctx)
+      | Polymorphic ctx ->
         assert(ContextSet.is_empty body_uctxs);
-        Polymorphic_const ctx
+        Polymorphic ctx
   in
   let ctx =
     UState.of_binders
@@ -580,11 +577,11 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
+        Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs
     | Some (c, ctx) ->
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
+        Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 3f7837fd6e..bc936975c2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -209,7 +209,7 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c ~priv =
+let pr_abstract_universe_ctx sigma ?variance ?priv c =
   let open Univ in
   let priv = Option.default Univ.ContextSet.empty priv in
   let has_priv = not (ContextSet.is_empty priv) in
@@ -221,23 +221,9 @@ let pr_abstract_universe_ctx sigma ?variance c ~priv =
   else
     mt()
 
-let pr_constant_universes sigma ~priv = function
-  | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
-  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
-
-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 (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
-  else
-    mt()
-
-let pr_abstract_cumulativity_info sigma cumi =
-  if !Detyping.print_universes
-  && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
-  else
-    mt()
+let pr_universes sigma ?variance ?priv = function
+  | Declarations.Monomorphic ctx -> pr_universe_ctx_set sigma ctx
+  | Declarations.Polymorphic ctx -> pr_abstract_universe_ctx sigma ?variance ?priv ctx
 
 (**********************************************************************)
 (* Global references *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 9a06d555e4..4e27268c4d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -86,11 +86,11 @@ val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Const
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
-  Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t
+  ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
-val pr_constant_universes  : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t
-val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
-val pr_abstract_cumulativity_info   : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
+val pr_universes  : evar_map ->
+  ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t ->
+  Declarations.universes -> Pp.t
 
 (** Printing global references using names as short as possible *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 898f231a8b..3438063f76 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -126,10 +126,7 @@ let print_mutual_inductive env mind mib udecl =
   hov 0 (def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
            (print_one_inductive env sigma mib) inds ++
-         match mib.mind_universes with
-         | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
-         | Cumulative_ind cumi ->
-           Printer.pr_abstract_cumulativity_info sigma cumi)
+         Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -178,10 +175,7 @@ let print_record env mind mib udecl =
         (fun (id,b,c) ->
           Id.print id ++ str (if b then " : " else " := ") ++
           Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
-    match mib.mind_universes with
-    | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
-    | Cumulative_ind cumi ->
-      Printer.pr_abstract_cumulativity_info sigma cumi
+    Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
   )
 
 let pr_mutual_inductive_body env mind mib udecl =
@@ -302,7 +296,7 @@ let print_body is_impl extent env mp (l,body) =
 		hov 2 (str ":= " ++
                        Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs)
+            Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs)
     | SFBmind mib ->
       match extent with
       | WithContents ->