[api] Remove aliases of `Evar.t`

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

7 files changed, 58 insertions, 58 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 14d07ccaeb..907f1b1acd 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 42f2d5f25a..5fd4634d67 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 60bd6de2ae..ecef04204e 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 17fa150454..aed2d7083b 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 7f7acf8745..59728a2fd1 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 46fac50f22..07fe902220 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 793490798a..c9a530076c 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