[api] Remove aliases of `Evar.t`

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

39 files changed, 175 insertions, 163 deletions

diff --git a/API/API.mli b/API/API.mli
index 1f1b05ead..fbdf680f3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -491,6 +491,8 @@ sig
 
   val equal : t -> t -> bool
 
+  val print : t -> Pp.t
+
   (** a set of unique identifiers of some {i evars} *)
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
@@ -516,12 +518,16 @@ sig
   type metavariable = int
 
   type existential_key = Evar.t
-  type 'constr pexistential = existential_key * 'constr array
+  [@@ocaml.deprecated "use Evar.t"]
+
+  type 'constr pexistential = Evar.t * 'constr array
 
   type 'a puniverses = 'a Univ.puniverses
-  type pconstant = Constant.t puniverses
-  type pinductive = inductive puniverses
-  type pconstructor = constructor puniverses
+  [@@ocaml.deprecated "use Univ.puniverses"]
+
+  type pconstant = Constant.t Univ.puniverses
+  type pinductive = inductive Univ.puniverses
+  type pconstructor = constructor Univ.puniverses
 
   type ('constr, 'types) prec_declaration =
     Name.t array * 'types array * 'constr array
@@ -594,7 +600,7 @@ sig
   val mkRel : int -> t
   val mkVar : Id.t -> t
   val mkMeta : metavariable -> t
-  type existential = existential_key * constr array
+  type existential = Evar.t * constr array
   val mkEvar : existential -> t
   val mkSort : Sorts.t -> t
   val mkProp : t
@@ -605,7 +611,7 @@ sig
   val mkLambda : Name.t * types * t -> t
   val mkLetIn : Name.t * t * types * t -> t
   val mkApp : t * t array -> t
-  val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+  val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
 
   type rec_declaration = Name.t array * types array * constr array
   type fixpoint = (int array * int) * rec_declaration
@@ -695,16 +701,16 @@ sig
   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
@@ -988,11 +994,11 @@ sig
 
   type 'a puniverses = 'a Univ.puniverses
   [@@ocaml.deprecated "Alias of Constr.puniverses"]
-  type pconstant = Names.Constant.t Constr.puniverses
+  type pconstant = Names.Constant.t Univ.puniverses
   [@@ocaml.deprecated "Alias of Constr.pconstant"]
-  type pinductive = Names.inductive Constr.puniverses
+  type pinductive = Names.inductive Univ.puniverses
   [@@ocaml.deprecated "Alias of Constr.pinductive"]
-  type pconstructor = Names.constructor Constr.puniverses
+  type pconstructor = Names.constructor Univ.puniverses
   [@@ocaml.deprecated "Alias of Constr.pconstructor"]
   type case_style = Constr.case_style =
     | LetStyle
@@ -1045,7 +1051,7 @@ sig
      | CoFix     of ('constr, 'types) Constr.pcofixpoint
      | Proj      of Names.Projection.t * 'constr
   [@@ocaml.deprecated "Alias of Constr.kind_of_term"]
-  type existential = Constr.existential_key * Constr.constr array
+  type existential = Evar.t * Constr.constr array
   [@@ocaml.deprecated "Alias of Constr.existential"]
   type rec_declaration = Names.Name.t array * Constr.constr array * Constr.constr array
   [@@ocaml.deprecated "Alias of Constr.rec_declaration"]
@@ -1093,7 +1099,7 @@ sig
   [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstruct : Names.constructor -> constr
   [@@ocaml.deprecated "Alias of similarly named Constr function"]
-  val mkConstructU : Names.constructor Constr.puniverses -> constr
+  val mkConstructU : Names.constructor Univ.puniverses -> constr
   [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstructUi : (Constr.pinductive * int) -> constr
   [@@ocaml.deprecated "Alias of similarly named Constr function"]
@@ -1135,7 +1141,7 @@ sig
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destRel : constr -> int
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
-  val destConst : constr -> Names.Constant.t Constr.puniverses
+  val destConst : constr -> Names.Constant.t Univ.puniverses
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val destCast : constr -> constr * Constr.cast_kind * constr
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
@@ -1208,7 +1214,7 @@ sig
   val is_prop_sort : Sorts.t -> bool
   [@@ocaml.deprecated "alias of API.Sorts.is_prop"]
 
-  type existential_key = Constr.existential_key
+  type existential_key = Evar.t
   [@@ocaml.deprecated "Alias of Constr.existential_key"]
 
   val family_of_sort : Sorts.t -> Sorts.family
@@ -1220,7 +1226,7 @@ sig
   val constr_ord : constr -> constr -> int
   [@@ocaml.deprecated "alias of Term.compare"]
 
-  val destInd : constr -> Names.inductive Constr.puniverses
+  val destInd : constr -> Names.inductive Univ.puniverses
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
   val univ_of_sort : Sorts.t -> Univ.Universe.t
   [@@ocaml.deprecated "Alias for the function in [Constr]"]
@@ -2186,7 +2192,7 @@ sig
          | ImpossibleCase
          | MatchingVar of matching_var_kind
          | VarInstance of Names.Id.t
-         | SubEvar of Constr.existential_key
+         | SubEvar of Evar.t
 end
 
 module Glob_term :
@@ -2772,9 +2778,12 @@ end
 module Evd :
 sig
 
-  type evar = Constr.existential_key
+  type evar = Evar.t
+  [@@ocaml.deprecated "use Evar.t"]
 
   val string_of_existential : Evar.t -> string
+  [@@ocaml.deprecated "use Evar.print"]
+
   type evar_constraint = Reduction.conv_pb * Environ.env * Constr.t * Constr.t
 
   (* --------------------------------- *)
@@ -2851,7 +2860,7 @@ sig
     val empty : evar_map
     val from_env : Environ.env -> evar_map
     val find : evar_map -> Evar.t -> evar_info
-    val find_undefined : evar_map -> evar -> evar_info
+    val find_undefined : evar_map -> Evar.t -> evar_info
     val is_defined : evar_map -> Evar.t -> bool
     val mem : evar_map -> Evar.t -> bool
     val add : evar_map -> Evar.t -> evar_info -> evar_map
@@ -2879,7 +2888,7 @@ sig
     val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 
     val universe_context_set : evar_map -> Univ.ContextSet.t
-    val evar_ident : evar -> evar_map -> Names.Id.t option
+    val evar_ident : Evar.t -> evar_map -> Names.Id.t option
     val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
     val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
                            (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
@@ -3311,7 +3320,7 @@ sig
     val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
     val read_line : string t
   end
-  val proofview : proofview -> Evd.evar list * Evd.evar_map
+  val proofview : proofview -> Evar.t list * Evd.evar_map
   val cycle : int -> unit tactic
   val swap : int -> int -> unit tactic
   val revgoals : unit tactic
@@ -3338,20 +3347,20 @@ sig
   val shelve_unifiable : unit tactic
   val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                      * proofview
-                                                     * (bool * Evd.evar list * Evd.evar list)
+                                                     * (bool * Evar.t list * Evar.t list)
                                                      * Proofview_monad.Info.tree
   val numgoals : int tactic
-  val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic
+  val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic
 
   module Unsafe :
   sig
     val tclEVARS : Evd.evar_map -> unit tactic
 
-    val tclGETGOALS : Evd.evar list tactic
+    val tclGETGOALS : Evar.t list tactic
 
-    val tclSETGOALS : Evd.evar list -> unit tactic
+    val tclSETGOALS : Evar.t list -> unit tactic
 
-    val tclNEWGOALS : Evd.evar list -> unit tactic
+    val tclNEWGOALS : Evar.t list -> unit tactic
   end
 
   module Goal :
@@ -3667,7 +3676,7 @@ sig
   val nconstructors : Names.inductive -> int
   val find_rectype : Environ.env -> Evd.evar_map -> EConstr.types -> inductive_type
   val get_constructors : Environ.env -> inductive_family -> constructor_summary array
-  val dest_ind_family : inductive_family -> Names.inductive Constr.puniverses * Constr.t list
+  val dest_ind_family : inductive_family -> Names.inductive Univ.puniverses * Constr.t list
   val find_inductive   : Environ.env -> Evd.evar_map -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * Constr.t list
   val type_of_inductive : Environ.env -> Constr.pinductive -> Constr.types
 end
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4e7b94e41..832040ad2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -18,7 +18,6 @@ open Univ
 open Environ
 open Printer
 open Constr
-open Evd
 open Goptions
 open Genarg
 open Clenv
@@ -62,7 +61,7 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 (* term printers *)
 let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
-let ppevar evk = pp (str (Evd.string_of_existential evk))
+let ppevar evk = pp (Evar.print evk)
 let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
 let ppeconstr x = pp (Termops.print_constr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
@@ -263,7 +262,7 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
+  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")"
   | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
       "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 14d07ccae..907f1b1ac 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -54,7 +54,7 @@ let new_global evd x =
 
 (* flush_and_check_evars fails if an existential is undefined *)
 
-exception Uninstantiated_evar of existential_key
+exception Uninstantiated_evar of Evar.t
 
 let rec flush_and_check_evars sigma c =
   match kind c with
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 42f2d5f25..5fd4634d6 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -38,9 +38,9 @@ val new_pure_evar :
   named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * evar
+  ?principal:bool -> types -> evar_map * Evar.t
 
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
+val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
 
 (** the same with side-effects *)
 val e_new_evar :
@@ -63,8 +63,8 @@ val e_new_type_evar : env -> evar_map ref ->
 val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
-val restrict_evar : evar_map -> existential_key -> Filter.t ->
-  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * existential_key
+val restrict_evar : evar_map -> Evar.t -> Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
 
 (** Polymorphic constants *)
 
@@ -96,7 +96,7 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** [head_evar c] returns the head evar of [c] if any *)
 exception NoHeadEvar
-val head_evar : evar_map -> constr -> existential_key (** may raise NoHeadEvar *)
+val head_evar : evar_map -> constr -> Evar.t (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
 val whd_head_evar :  evar_map -> constr -> constr
@@ -116,13 +116,13 @@ val is_ground_env  :  evar_map -> env -> bool
     associating to each dependent evar [None] if it has no (partial)
     definition or [Some s] if [s] is the list of evars appearing in
     its (partial) definition. *)
-val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
+val gather_dependent_evars : evar_map -> Evar.t list -> (Evar.Set.t option) Evar.Map.t
 
 (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
     the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially)
     solved. *)
-val advance : evar_map -> evar -> evar option
+val advance : evar_map -> Evar.t -> Evar.t option
 
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
@@ -177,7 +177,7 @@ val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr)
 val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
-exception Uninstantiated_evar of existential_key
+exception Uninstantiated_evar of Evar.t
 val flush_and_check_evars :  evar_map -> constr -> Constr.constr
 
 (** {6 Term manipulation up to instantiation} *)
@@ -233,7 +233,7 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
 
-val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
+val subterm_source : Evar.t -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
 val meta_counter_summary_name : string
diff --git a/engine/evd.ml b/engine/evd.ml
index 60bd6de2a..ecef04204 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -127,7 +127,7 @@ end
 
 module Store = Store.Make ()
 
-type evar = existential_key
+type evar = Evar.t
 
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
@@ -371,7 +371,7 @@ val key : Id.t -> t -> Evar.t
 end =
 struct
 
-type t = Id.t EvMap.t * existential_key Id.Map.t
+type t = Id.t EvMap.t * Evar.t Id.Map.t
 
 let empty = (EvMap.empty, Id.Map.empty)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 17fa15045..aed2d7083 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -28,12 +28,13 @@ open Environ
 
 (** {5 Existential variables and unification states} *)
 
-(** {6 Evars} *)
-
-type evar = existential_key
+type evar = Evar.t
+[@@ocaml.deprecated "use Evar.t"]
 (** Existential variables. *)
 
-val string_of_existential : evar -> string
+(** {6 Evars} *)
+val string_of_existential : Evar.t -> string
+[@@ocaml.deprecated "use Evar.print"]
 
 (** {6 Evar filters} *)
 
@@ -150,44 +151,44 @@ val has_undefined : evar_map -> bool
     there are uninstantiated evars in [sigma]. *)
 
 val new_evar : evar_map ->
-  ?name:Id.t -> evar_info -> evar_map * evar
+  ?name:Id.t -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
 
-val add : evar_map -> evar -> evar_info -> evar_map
+val add : evar_map -> Evar.t -> evar_info -> evar_map
 (** [add sigma ev info] adds [ev] with evar info [info] in sigma.
     Precondition: ev must not preexist in [sigma]. *)
 
-val find : evar_map -> evar -> evar_info
+val find : evar_map -> Evar.t -> evar_info
 (** Recover the data associated to an evar. *)
 
-val find_undefined : evar_map -> evar -> evar_info
+val find_undefined : evar_map -> Evar.t -> evar_info
 (** Same as {!find} but restricted to undefined evars. For efficiency
     reasons. *)
 
-val remove : evar_map -> evar -> evar_map
+val remove : evar_map -> Evar.t -> evar_map
 (** Remove an evar from an evar map. Use with caution. *)
 
-val mem : evar_map -> evar -> bool
+val mem : evar_map -> Evar.t -> bool
 (** Whether an evar is present in an evarmap. *)
 
-val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+val fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 (** Apply a function to all evars and their associated info in an evarmap. *)
 
-val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 (** Same as {!fold}, but restricted to undefined evars. For efficiency
     reasons. *)
 
-val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+val raw_map : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map
 (** Apply the given function to all evars in the map. Beware: this function
     expects the argument function to preserve the kind of [evar_body], i.e. it
     must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some
     [Evar_defined c']. *)
 
-val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map
+val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map
 (** Same as {!raw_map}, but restricted to undefined evars. For efficiency
     reasons. *)
 
-val define : evar -> constr -> evar_map -> evar_map
+val define : Evar.t-> constr -> evar_map -> evar_map
 (** Set the body of an evar to the given constr. It is expected that:
     {ul
       {- The evar is already present in the evarmap.}
@@ -198,13 +199,13 @@ val define : evar -> constr -> evar_map -> evar_map
 val cmap : (constr -> constr) -> evar_map -> evar_map
 (** Map the function on all terms in the evar map. *)
 
-val is_evar : evar_map -> evar -> bool
+val is_evar : evar_map -> Evar.t-> bool
 (** Alias for {!mem}. *)
 
-val is_defined : evar_map -> evar -> bool
+val is_defined : evar_map -> Evar.t-> bool
 (** Whether an evar is defined in an evarmap. *)
 
-val is_undefined : evar_map -> evar -> bool
+val is_undefined : evar_map -> Evar.t-> bool
 (** Whether an evar is not defined in an evarmap. *)
 
 val add_constraints : evar_map -> Univ.constraints -> evar_map
@@ -240,31 +241,31 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 (** {6 Misc} *)
 
-val restrict : evar -> Filter.t -> ?candidates:constr list ->
-  ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
+val restrict : Evar.t-> Filter.t -> ?candidates:constr list ->
+  ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
-val is_restricted_evar : evar_info -> evar option
+val is_restricted_evar : evar_info -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
-val downcast : evar -> types -> evar_map -> evar_map
+val downcast : Evar.t-> types -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
 
-val evar_source : existential_key -> evar_map -> Evar_kinds.t located
+val evar_source : Evar.t -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
-val evar_ident : existential_key -> evar_map -> Id.t option
+val evar_ident : Evar.t -> evar_map -> Id.t option
 
-val rename : existential_key -> Id.t -> evar_map -> evar_map
+val rename : Evar.t -> Id.t -> evar_map -> evar_map
 
-val evar_key : Id.t -> evar_map -> existential_key
+val evar_key : Id.t -> evar_map -> Evar.t
 
 val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located
 
-val dependent_evar_ident : existential_key -> evar_map -> Id.t
+val dependent_evar_ident : Evar.t -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7f7acf874..59728a2fd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -25,7 +25,7 @@ type proofview
    new nearly identical function everytime. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
-val proofview : proofview -> Evd.evar list * Evd.evar_map
+val proofview : proofview -> Evar.t list * Evd.evar_map
 
 
 (** {6 Starting and querying a proof view} *)
@@ -88,7 +88,7 @@ type focus_context
    new nearly identical function everytime. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
-val focus_context : focus_context -> Evd.evar list * Evd.evar list
+val focus_context : focus_context -> Evar.t list * Evar.t list
 
 (** [focus i j] focuses a proofview on the goals from index [i] to
     index [j] (inclusive, goals are indexed from [1]). I.e. goals
@@ -148,7 +148,7 @@ type +'a tactic
     {!Logic_monad.TacticFailure}*)
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
-                                                   * (bool*Evd.evar list*Evd.evar list)
+                                                   * (bool*Evar.t list*Evar.t list)
                                                    * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
@@ -304,12 +304,12 @@ val shelve : unit tactic
 (** Shelves the given list of goals, which might include some that are
     under focus and some that aren't. All the goals are placed on the
     shelf for later use (or being solved by side-effects). *)
-val shelve_goals : Evd.evar list -> unit tactic
+val shelve_goals : Evar.t list -> unit tactic
 
 (** [unifiable sigma g l] checks whether [g] appears in another
     subgoal of [l]. The list [l] may contain [g], but it does not
     affect the result. Used by [shelve_unifiable]. *)
-val unifiable : Evd.evar_map -> Evd.evar -> Evd.evar list -> bool
+val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
 
 (** Shelves the unifiable goals under focus, i.e. the goals which
     appear in other goals under focus (the unfocused goals are not
@@ -322,15 +322,15 @@ val guard_no_unifiable : Names.Name.t list option tactic
 
 (** [unshelve l p] adds all the goals in [l] at the end of the focused
     goals of p *)
-val unshelve : Evd.evar list -> proofview -> proofview
+val unshelve : Evar.t list -> proofview -> proofview
 
 (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
-val depends_on : Evd.evar_map -> Evd.evar -> Evd.evar -> bool
+val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool
 
 (** [with_shelf tac] executes [tac] and returns its result together with
     the set of goals shelved by [tac]. The current shelf is unchanged
     and the returned list contains only unsolved goals. *)
-val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic
+val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic
 
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
     is negative, then it puts the [n] last goals first.*)
@@ -416,14 +416,14 @@ module Unsafe : sig
   (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
       being proved, appending them to the list of focused goals. If a
       goal is already solved, it is not added. *)
-  val tclNEWGOALS : Evd.evar list -> unit tactic
+  val tclNEWGOALS : Evar.t list -> unit tactic
 
   (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
       goal is already solved, it is not set. *)
-  val tclSETGOALS : Evd.evar list -> unit tactic
+  val tclSETGOALS : Evar.t list -> unit tactic
 
   (** [tclGETGOALS] returns the list of goals under focus. *)
-  val tclGETGOALS : Evd.evar list tactic
+  val tclGETGOALS : Evar.t list tactic
 
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
@@ -566,9 +566,9 @@ module V82 : sig
   [@@ocaml.deprecated "Use [Proofview.proofview]"]
 
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
-  
+
   (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evd.evar list
+  val top_evars : entry -> Evar.t list
 
   (* Caution: this function loses quite a bit of information. It
      should be avoided as much as possible.  It should work as
diff --git a/engine/termops.ml b/engine/termops.ml
index 46fac50f2..07fe90222 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -205,8 +205,7 @@ let pr_evar_source = function
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id
   | Evar_kinds.SubEvar evk ->
-      let open Evd in
-      str "subterm of " ++ str (string_of_existential evk)
+    str "subterm of " ++ Evar.print evk
 
 let pr_evar_info evi =
   let open Evd in
@@ -356,7 +355,7 @@ let pr_evar_map_gen with_univs pr_evars sigma =
 let pr_evar_list sigma l =
   let open Evd in
   let pr (ev, evi) =
-    h 0 (str (string_of_existential ev) ++
+    h 0 (Evar.print ev ++
       str "==" ++ pr_evar_info evi ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
diff --git a/engine/termops.mli b/engine/termops.mli
index 793490798..c9a530076 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -91,7 +91,7 @@ exception Occur
 val occur_meta : Evd.evar_map -> constr -> bool
 val occur_existential : Evd.evar_map -> constr -> bool
 val occur_meta_or_existential : Evd.evar_map -> constr -> bool
-val occur_evar : Evd.evar_map -> existential_key -> constr -> bool
+val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_in_decl :
   env -> Evd.evar_map ->
@@ -281,9 +281,9 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 open Evd
 
-val pr_existential_key : evar_map -> evar -> Pp.t
+val pr_existential_key : evar_map -> Evar.t -> Pp.t
 
-val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t
 
 val pr_evar_info : evar_info -> Pp.t
 val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml
index 36c421c6c..428d6b678 100644
--- a/intf/evar_kinds.ml
+++ b/intf/evar_kinds.ml
@@ -32,4 +32,4 @@ type t =
   | ImpossibleCase
   | MatchingVar of matching_var_kind
   | VarInstance of Id.t
-  | SubEvar of Constr.existential_key
+  | SubEvar of Evar.t
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
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 83b454769..047ca509b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -565,7 +565,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   if evlist = [] then 0, c0 else
   let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
-    (fun (k,_) -> str(Evd.string_of_existential k)) evlist));
+    (fun (k,_) -> Evar.print k) evlist));
   let evplist = 
     let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
         let t = EConstr.of_constr t in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 276b7c8ab..e63a05b78 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -396,7 +396,7 @@ let inv_dir = function L2R -> R2L | R2L -> L2R
 type pattern_class =
   | KpatFixed
   | KpatConst
-  | KpatEvar of existential_key
+  | KpatEvar of Evar.t
   | KpatLet
   | KpatLam
   | KpatRigid
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 95de96926..192eca63b 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 5f9609a5c..1d4c88ea2 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 e5d288b5c..703c4616c 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 febe99b0b..58b1ce6c3 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 ce478ac20..7149d62a1 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 dab376ef0..430755ea0 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 e3470b0f1..eb90e5fe0 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 b2735ee22..838938524 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 d55b286fb..2e213a51d 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 062d5cf35..618826f3d 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
diff --git a/printing/printer.ml b/printing/printer.ml
index d7bb0460d..3d40c104e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -583,7 +583,7 @@ let default_pr_subgoal n sigma =
   in
   prrec n
 
-let pr_internal_existential_key ev = str (string_of_existential ev)
+let pr_internal_existential_key ev = Evar.print ev
 
 let print_evar_constraints gl sigma =
   let pr_env =
@@ -762,7 +762,7 @@ let default_pr_subgoals ?(pr_first=true)
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
  pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
  pr_goal                : goal sigma -> Pp.t;
 }
diff --git a/printing/printer.mli b/printing/printer.mli
index e014baa2c..5adc0e858 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -129,7 +129,7 @@ val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
 val pr_global              : global_reference -> Pp.t
 
 val pr_constant            : env -> Constant.t -> Pp.t
-val pr_existential_key     : evar_map -> existential_key -> Pp.t
+val pr_existential_key     : evar_map -> Evar.t -> Pp.t
 val pr_existential         : env -> evar_map -> existential -> Pp.t
 val pr_constructor         : env -> constructor -> Pp.t
 val pr_inductive           : env -> inductive -> Pp.t
@@ -178,7 +178,7 @@ val pr_goal                : goal sigma -> Pp.t
    focused goals unless the conrresponding option
    [enable_unfocused_goal_printing] is set. [seeds] is for printing
    dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list
+val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list
                              -> goal list -> goal list -> Pp.t
 
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
@@ -186,7 +186,7 @@ val pr_concl               : int -> evar_map -> goal -> Pp.t
 
 val pr_open_subgoals       : proof:Proof.proof -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.proof -> int -> Pp.t
-val pr_evar                : evar_map -> (evar * evar_info) -> Pp.t
+val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
@@ -221,7 +221,7 @@ val pr_assumptionset :
 val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
  pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
  pr_goal                : goal sigma -> Pp.t;
 }
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a0e3b718a..d90cff572 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -14,5 +14,5 @@ open Ltac_pretype
 
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
-val w_refine : evar * evar_info ->
+val w_refine : Evar.t * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 19f816a01..d5bc7e0ce 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -16,7 +16,7 @@ module NamedDecl = Context.Named.Declaration
    evar is defined in the current evar_map, should not be accessed. *)
 
 (* type of the goals *)
-type goal = Evd.evar
+type goal = Evar.t
 
 let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5756d06b6..83777fc96 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -194,7 +194,7 @@ module V82 : sig
   val top_goal : proof -> Goal.goal Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : proof -> Evd.evar list
+  val top_evars : proof -> Evar.t list
 
   (* Turns the unresolved evars into goals.
      Raises [UnfinishedProof] if there are still unsolved goals. *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a44de66e9..700fd6045 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -155,7 +155,7 @@ let evar_dependencies evm oev =
       let evi = Evd.find evm ev in
       let deps' = evars_of_filtered_evar_info evi in
       if Evar.Set.mem oev deps' then
-	invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
+        invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
       else Evar.Set.union deps' s)
       deps deps
   in
@@ -164,7 +164,7 @@ let evar_dependencies evm oev =
       if Evar.Set.equal deps deps' then deps
       else aux deps'
   in aux (Evar.Set.singleton oev)
-      
+
 let move_after (id, ev, deps as obl) l = 
   let rec aux restdeps = function
     | (id', _, _) as obl' :: tl -> 
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 481faadb8..0602e52e9 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -32,7 +32,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
-  * ((existential_key * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+  * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
     constr * types
     (* Translations from existential identifiers to obligation identifiers 
        and for terms with existentials to closed terms, given a