From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 printing/printer.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing/printer.mli')

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 *)
 
-- 
cgit v1.2.3