[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, 29 insertions, 31 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 95de969260..192eca63bb 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -45,7 +45,7 @@ type cbv_value =
   | LAM of int * (Name.t * constr) list * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
-  | CONSTR of constructor puniverses * cbv_value array
+  | CONSTR of constructor Univ.puniverses * cbv_value array
 
 (* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 5f9609a5c5..1d4c88ea22 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -33,7 +33,7 @@ type cbv_value =
   | LAM of int * (Name.t * constr) list * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
-  | CONSTR of constructor puniverses * cbv_value array
+  | CONSTR of constructor Univ.puniverses * cbv_value array
 
 and cbv_stack =
   | TOP
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index e5d288b5c3..703c4616c7 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constr
 open EConstr
 open Evd
 open Environ
@@ -49,7 +48,7 @@ val refresh_universes :
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
-  bool option -> existential_key -> constr array -> constr array -> evar_map
+  bool option -> Evar.t -> constr array -> constr array -> evar_map
 
 val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
@@ -78,10 +77,10 @@ exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
 val check_evar_instance :
-  evar_map -> existential_key -> constr -> conv_fun -> evar_map
+  evar_map -> Evar.t -> constr -> conv_fun -> evar_map
 
 val remove_instance_local_defs :
-  evar_map -> existential_key -> 'a array -> 'a list
+  evar_map -> Evar.t -> 'a array -> 'a list
 
 val get_type_of_refresh : 
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index febe99b0bc..58b1ce6c3f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -28,8 +28,8 @@ val arities_of_constructors : env -> pinductive -> types array
     reasoning either with only recursively uniform parameters or with all
     parameters including the recursively non-uniform ones *)
 type inductive_family
-val make_ind_family : inductive puniverses * constr list -> inductive_family
-val dest_ind_family : inductive_family -> inductive puniverses * constr list
+val make_ind_family : inductive Univ.puniverses * constr list -> inductive_family
+val dest_ind_family : inductive_family -> inductive Univ.puniverses * constr list
 val map_ind_family : (constr -> constr) -> inductive_family -> inductive_family
 val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
 val lift_inductive_family  : int -> inductive_family -> inductive_family
@@ -195,7 +195,7 @@ i*)
 (********************)
 
 val type_of_inductive_knowing_conclusion :
-  env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types
+  env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types
 
 (********************)
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ce478ac202..7149d62a19 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -7,20 +7,19 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Environ
 open EConstr
 open Type_errors
 
 type unification_error =
-  | OccurCheck of existential_key * constr
+  | OccurCheck of Evar.t * constr
   | NotClean of existential * env * constr (* Constr is a variable not in scope *)
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
-  | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key * env * types * types
+  | MetaOccurInBody of Evar.t
+  | InstanceNotSameType of Evar.t * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
   | ProblemBeyondCapabilities
@@ -39,8 +38,8 @@ type pretype_error =
   (* Type inference unification *)
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (* Tactic unification *)
-  | UnifOccurCheck of existential_key * constr
-  | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
+  | UnifOccurCheck of Evar.t * constr
+  | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -57,7 +56,7 @@ type pretype_error =
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
-    (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (Evar.t * Evar_kinds.t) option * Evar.Set.t option
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index dab376ef07..430755ea04 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -15,14 +15,14 @@ open Type_errors
 (** {6 The type of errors raised by the pretyper } *)
 
 type unification_error =
-  | OccurCheck of existential_key * constr
+  | OccurCheck of Evar.t * constr
   | NotClean of existential * env * constr
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr
-  | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key * env * types * types
+  | MetaOccurInBody of Evar.t
+  | InstanceNotSameType of Evar.t * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
   | ProblemBeyondCapabilities
@@ -41,8 +41,8 @@ type pretype_error =
   (** Type inference unification *)
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (** Tactic Unification *)
-  | UnifOccurCheck of existential_key * constr
-  | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
+  | UnifOccurCheck of Evar.t * constr
+  | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -59,7 +59,7 @@ type pretype_error =
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
-    (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (Evar.t * Evar_kinds.t) option * Evar.Set.t option
     (** unresolvable evar, connex component *)
 
 exception PretypeError of env * Evd.evar_map * pretype_error
@@ -112,10 +112,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 (** {6 Implicit arguments synthesis errors } *)
 
-val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
+val error_occur_check : env -> Evd.evar_map -> Evar.t -> constr -> 'b
 
 val error_unsolvable_implicit :
-  ?loc:Loc.t -> env -> Evd.evar_map -> existential_key ->
+  ?loc:Loc.t -> env -> Evd.evar_map -> Evar.t ->
       Evd.unsolvability_explanation option -> 'b
 
 val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
@@ -154,7 +154,7 @@ val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
 
 (** {6 Typeclass errors } *)
 
-val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option ->
+val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option ->
   Evar.Set.t option -> 'a
 
 val unsatisfiable_exception : exn -> bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3470b0f11..eb90e5fe07 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -223,7 +223,7 @@ let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
 
-type inference_hook = env -> evar_map -> evar -> evar_map * constr
+type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b2735ee22c..8389385246 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,7 +27,7 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type inference_hook = env -> evar_map -> evar -> evar_map * constr
+type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d55b286fb4..2e213a51d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -521,7 +521,7 @@ let mark_unresolvable evi = mark_resolvability false evi
 let mark_resolvable evi = mark_resolvability true evi
 
 open Evar_kinds
-type evar_filter = existential_key -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t -> bool
 
 let all_evars _ _ = true
 let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 062d5cf356..618826f3d0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -68,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list
 
 (** Get the instantiated typeclass structure for a given universe instance. *)
-val typeclass_univ_instance : typeclass puniverses -> typeclass
+val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
 
 (** Just return None if not a class *)
 val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
@@ -83,11 +83,11 @@ val is_instance : global_reference -> bool
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
-val instance_constructor : typeclass puniverses -> constr list -> 
+val instance_constructor : typeclass Univ.puniverses -> constr list ->
   constr option * types
 
 (** Filter which evars to consider for resolution. *)
-type evar_filter = existential_key -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t -> bool
 val all_evars : evar_filter
 val all_goals : evar_filter
 val no_goals : evar_filter