[api] Remove aliases of `Evar.t`

There don't really bring anything, we also correct some minor nits
with the printing function.

10 files changed, 34 insertions, 28 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fa12e5406..31ded9129 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -234,7 +234,7 @@ let unfold_red kn =
  * instantiations (cbv or lazy) are.
  *)
 
-type table_key = Constant.t puniverses tableKey
+type table_key = Constant.t Univ.puniverses tableKey
 
 let eq_pconstant_key (c,u) (c',u') =
   eq_constant_key c c' && Univ.Instance.equal u u'
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 28136e1fc..119b70e30 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -92,7 +92,7 @@ val unfold_side_red : reds
 val unfold_red : evaluable_global_reference -> reds
 
 (***********************************************************************)
-type table_key = Constant.t puniverses tableKey
+type table_key = Constant.t Univ.puniverses tableKey
 
 type 'a infos_cache
 type 'a infos = {
@@ -122,8 +122,8 @@ type fterm =
   | FAtom of constr (** Metas and Sorts *)
   | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
-  | FInd of inductive puniverses
-  | FConstruct of constructor puniverses
+  | FInd of inductive Univ.puniverses
+  | FConstruct of constructor Univ.puniverses
   | FApp of fconstr * fconstr array
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 4c5ea9e95..21c477578 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -13,20 +13,22 @@ open Names
 
 (** {6 Value under universe substitution } *)
 type 'a puniverses = 'a Univ.puniverses
+[@@ocaml.deprecated "use Univ.puniverses"]
 
 (** {6 Simply type aliases } *)
-type pconstant = Constant.t puniverses
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
+type pconstant = Constant.t Univ.puniverses
+type pinductive = inductive Univ.puniverses
+type pconstructor = constructor Univ.puniverses
 
 (** {6 Existential variables } *)
 type existential_key = Evar.t
+[@@ocaml.deprecated "use Evar.t"]
 
 (** {6 Existential variables } *)
 type metavariable = int
 
 (** {6 Case annotation } *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
   { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
@@ -80,7 +82,7 @@ val mkVar : Id.t -> constr
 val mkMeta : metavariable -> constr
 
 (** Constructs an existential variable *)
-type existential = existential_key * constr array
+type existential = Evar.t * constr array
 val mkEvar : existential -> constr
 
 (** Construct a sort *)
@@ -111,7 +113,7 @@ val mkLetIn : Name.t * constr * types * constr -> constr
     {%latex:$(f~t_1\dots f_n)$%}. *)
 val mkApp : constr * constr array -> constr
 
-val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
 
 (** Constructs a Constant.t *)
 val mkConst : Constant.t -> constr
@@ -180,7 +182,7 @@ val mkCoFix : cofixpoint -> constr
 
 (** [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type 'constr pexistential = Evar.t * 'constr array
 type ('constr, 'types) prec_declaration =
     Name.t array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
@@ -295,16 +297,16 @@ val decompose_app : constr -> constr * constr list
 val decompose_appvect : constr -> constr * constr array
 
 (** Destructs a constant *)
-val destConst : constr -> Constant.t puniverses
+val destConst : constr -> Constant.t Univ.puniverses
 
 (** Destructs an existential variable *)
 val destEvar : constr -> existential
 
 (** Destructs a (co)inductive type *)
-val destInd : constr -> inductive puniverses
+val destInd : constr -> inductive Univ.puniverses
 
 (** Destructs a constructor *)
-val destConstruct : constr -> constructor puniverses
+val destConstruct : constr -> constructor Univ.puniverses
 
 (** Destructs a [match c as x in I args return P with ... |
 Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f2066b065..652ed0f9f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Constr
+open Univ
 open Declarations
 
 (** Unsafe environments. We define here a datatype for environments.
diff --git a/kernel/evar.ml b/kernel/evar.ml
index e63665f51..dcd2e12a0 100644
--- a/kernel/evar.ml
+++ b/kernel/evar.ml
@@ -13,6 +13,7 @@ let unsafe_of_int x = x
 let compare = Int.compare
 let equal = Int.equal
 let hash = Int.hash
+let print x = Pp.(str "?X" ++ int x)
 
 module Set = Int.Set
 module Map = Int.Map
diff --git a/kernel/evar.mli b/kernel/evar.mli
index eee6680fb..6a058207f 100644
--- a/kernel/evar.mli
+++ b/kernel/evar.mli
@@ -30,5 +30,8 @@ val compare : t -> t -> int
 val hash : t -> int
 (** Hash over existential variables. *)
 
+val print : t -> Pp.t
+(** Printing representation *)
+
 module Set : Set.S with type elt = t
 module Map : CMap.ExtS with type key = t and module Set := Set
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 601422a10..a19f87b05 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Constr
+open Univ
 open Declarations
 open Environ
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 4217cfac7..aa8805952 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -31,7 +31,7 @@ type constr = Constr.t
 type types = Constr.t
 (** Same as [constr], for documentation purposes. *)
 
-type existential_key = Constr.existential_key
+type existential_key = Evar.t
 type existential = Constr.existential
 
 type metavariable = Constr.metavariable
diff --git a/kernel/term.mli b/kernel/term.mli
index 4efb582d0..f5cb72f4e 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -129,7 +129,7 @@ val decompose_appvect : constr -> constr * constr array
 [@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"]
 
 (** Destructs a constant *)
-val destConst : constr -> Constant.t puniverses
+val destConst : constr -> Constant.t Univ.puniverses
 [@@ocaml.deprecated "Alias for [Constr.destConst]"]
 
 (** Destructs an existential variable *)
@@ -137,11 +137,11 @@ val destEvar : constr -> existential
 [@@ocaml.deprecated "Alias for [Constr.destEvar]"]
 
 (** Destructs a (co)inductive type *)
-val destInd : constr -> inductive puniverses
+val destInd : constr -> inductive Univ.puniverses
 [@@ocaml.deprecated "Alias for [Constr.destInd]"]
 
 (** Destructs a constructor *)
-val destConstruct : constr -> constructor puniverses
+val destConstruct : constr -> constructor Univ.puniverses
 [@@ocaml.deprecated "Alias for [Constr.destConstruct]"]
 
 (** Destructs a [match c as x in I args return P with ... |
@@ -407,11 +407,11 @@ val mkInd : inductive -> constr
 [@@ocaml.deprecated "Alias for Constr"]
 val mkConstruct : constructor -> constr
 [@@ocaml.deprecated "Alias for Constr"]
-val mkConstU : Constant.t puniverses -> constr
+val mkConstU : Constant.t Univ.puniverses -> constr
 [@@ocaml.deprecated "Alias for Constr"]
-val mkIndU : inductive puniverses -> constr
+val mkIndU : inductive Univ.puniverses -> constr
 [@@ocaml.deprecated "Alias for Constr"]
-val mkConstructU : constructor puniverses -> constr
+val mkConstructU : constructor Univ.puniverses -> constr
 [@@ocaml.deprecated "Alias for Constr"]
 val mkConstructUi : (pinductive * int) -> constr
 [@@ocaml.deprecated "Alias for Constr"]
@@ -461,7 +461,7 @@ val map_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
 [@@ocaml.deprecated "Alias for [Constr.map_with_binders]"]
 
-val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
 [@@ocaml.deprecated "Alias for [Constr.map_puniverses]"]
 val univ_of_sort : Sorts.t -> Univ.Universe.t
 [@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"]
@@ -497,7 +497,7 @@ type sorts = Sorts.t =
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
-type 'a puniverses = 'a Constr.puniverses
+type 'a puniverses = 'a Univ.puniverses
 [@@ocaml.deprecated "Alias for Constr.puniverses"]
 
 (** Simply type aliases *)
@@ -507,8 +507,8 @@ type pinductive = Constr.pinductive
 [@@ocaml.deprecated "Alias for Constr.pinductive"]
 type pconstructor = Constr.pconstructor
 [@@ocaml.deprecated "Alias for Constr.pconstructor"]
-type existential_key = Constr.existential_key
-[@@ocaml.deprecated "Alias for Constr.existential_key"]
+type existential_key = Evar.t
+[@@ocaml.deprecated "Alias for Evar.t"]
 type existential = Constr.existential
 [@@ocaml.deprecated "Alias for Constr.existential"]
 type metavariable = Constr.metavariable
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3aaad5877..5584b6ab4 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Constr
+open Univ
 open Environ
 open Entries