Universe instance printer: add optional variance argument.

1 files changed, 23 insertions, 19 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index e8f5ba568..77ebf5a11 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,6 +238,20 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val sup : t -> t -> t
+
+  val pr : t -> Pp.t
+
+end
+
 (** {6 Universe instances} *)
 
 module Instance :
@@ -273,7 +287,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -347,22 +361,6 @@ end
 type abstract_universe_context = AUContext.t
 [@@ocaml.deprecated "Use AUContext.t"]
 
-module Variance :
-sig
-  (** A universe position in the instance given to a cumulative
-     inductive can be the following. Note there is no Contravariant
-     case because [forall x : A, B <= forall x : A', B'] requires [A =
-     A'] as opposed to [A' <= A]. *)
-  type t = Irrelevant | Covariant | Invariant
-
-  val sup : t -> t -> t
-
-  val pr : t -> Pp.t
-
-  val leq_constraints : t array -> Instance.t constraint_function
-  val eq_constraints : t array -> Instance.t constraint_function
-end
-
 (** Universe info for cumulative inductive types: A context of
    universe levels with universe constraints, representing local
    universe variables and constraints, together with an array of
@@ -387,6 +385,8 @@ sig
      trivial subtyping relation. *)
   val from_universe_context : UContext.t -> t
 
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type cumulativity_info = CumulativityInfo.t
@@ -398,6 +398,8 @@ sig
 
   val univ_context : t -> AUContext.t
   val variance : t -> Variance.t array
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type abstract_cumulativity_info = ACumulativityInfo.t
@@ -491,9 +493,11 @@ val make_abstract_instance : AUContext.t -> Instance.t
 
 val pr_constraint_type : constraint_type -> Pp.t
 val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
-val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  UContext.t -> Pp.t
 val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
-val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  AUContext.t -> Pp.t
 val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
 val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
 val explain_universe_inconsistency : (Level.t -> Pp.t) ->