At least made the evar type opaque! There are still 5 remaining unsafe

casts of ints to evars.

- 2 in Evarutil and Goal which are really needed, even though the Goal
one could (and should) be removed;
- 2 in G_xml and Detyping that are there for completeness sake, but
that might be made anomalies altogether;
- 1 in Newring which is quite dubious at best, and should be fixed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 132 insertions, 141 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9483f0220..1588856f7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -391,7 +391,7 @@ let rec detype (isgoal:bool) avoid env t =
 	 in GVar (dl, Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
-	GEvar (dl, n, None)
+	GEvar (dl, Evar.unsafe_of_int n, None)
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id)
 	 with Not_found -> GVar (dl, id))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7724261ec..6d4f214cc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -338,7 +338,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  |_, (UnifFailure _ as x) -> x
 	  |Some _, _ -> UnifFailure (i,NotSameArgSize)
 	and f2 i =
-          if Int.equal sp1 sp2 then
+          if Evar.equal sp1 sp2 then
 	    match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
 	    |None, Success i' ->
               Success (solve_refl (fun env i pbty a1 a2 ->
@@ -805,7 +805,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (match choose_less_dependent_instance evk2 evd term1 args2 with
       | Some evd -> Success evd
       | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
-  | Evar (evk1,args1), Evar (evk2,args2) when Int.equal evk1 evk2 ->
+  | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
       let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in
       Success (solve_refl ~can_drop:true f env evd evk1 args1 args2)
   | Evar ev1, Evar ev2 ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 52088af38..a1bf6eabb 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -114,7 +114,7 @@ let noccur_evar env evd evk c =
       (match safe_evar_value evd ev' with
        | Some c -> occur_rec k c
        | None ->
-           if Int.equal evk evk' then raise Occur
+           if Evar.equal evk evk' then raise Occur
            else Array.iter (occur_rec k) args')
   | Rel i when i > k ->
       (match pi2 (Environ.lookup_rel (i-k) env) with
@@ -956,7 +956,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
       Array.for_all (is_constrainable_in k g) params
   | Ind _ -> Array.for_all (is_constrainable_in k g) args
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
-  | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+  | Evar (ev',_) -> not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
@@ -1068,7 +1068,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
   let candidates = filter_candidates evd evk untypedfilter None in
   let filter = closure_of_filter evd evk untypedfilter in
   let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
-  if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
+  if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
     (* either progress, or not allowed to drop, e.g. to preserve possibly *)
     (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
     (* if e can depend on x until ?y is not resolved, or, conversely, we *)
@@ -1198,7 +1198,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
           try project_variable t
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
     | Evar (evk',args' as ev') ->
-        if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs));
+        if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs));
         (* Evar/Evar problem (but left evar is virtual) *)
         let aliases = lift_aliases k aliases in
         (try
@@ -1278,7 +1278,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
   match kind_of_term rhs with
   | Evar (evk2,argsv2 as ev2) ->
-      if Int.equal evk evk2 then
+      if Evar.equal evk evk2 then
         solve_refl ~can_drop:choose
           (test_success conv_algo) env evd evk argsv argsv2
       else
@@ -1322,7 +1322,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
         (* last chance: rhs actually reduces to ev *)
         let c = whd_betadeltaiota env evd rhs in
         match kind_of_term c with
-        | Evar (evk',argsv2) when Int.equal evk evk' ->
+        | Evar (evk',argsv2) when Evar.equal evk evk' ->
 	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
               env evd evk argsv argsv2
         | _ ->
@@ -1355,8 +1355,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
  *)
 
 let status_changed lev (pbty,_,t1,t2) =
-  (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
-  (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
+  (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) or
+  (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
 
 let reconsider_conv_pbs conv_algo evd =
   let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b1dec0fd0..f66e5f708 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -233,7 +233,7 @@ let evars_to_metas sigma (emap, c) =
 
 let non_instantiated sigma =
   let listev = Evd.undefined_map sigma in
-  ExistentialMap.map (fun evi -> nf_evar_info sigma evi) listev
+  Evar.Map.map (fun evi -> nf_evar_info sigma evi) listev
 
 (************************)
 (* Manipulating filters *)
@@ -257,7 +257,7 @@ let make_pure_subst evi args =
 (* Generator of existential names *)
 let new_untyped_evar =
   let evar_ctr = Summary.ref 0 ~name:"evar counter" in
-  fun () -> incr evar_ctr; existential_of_int !evar_ctr
+  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
  * functional operations on evar sets *
@@ -486,14 +486,14 @@ let clear_hyps_in_evi evdref hyps concl ids =
 let evars_of_term c =
   let rec evrec acc c =
     match kind_of_term c with
-    | Evar (n, l) -> Int.Set.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
     | _ -> fold_constr evrec acc c
   in
-  evrec Int.Set.empty c
+  evrec Evar.Set.empty c
 
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
-  Int.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
+  Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
 let queue_term q is_dependent c =
   queue_set q is_dependent (evars_of_term c)
 
@@ -510,7 +510,7 @@ let process_dependent_evar q acc evm is_dependent e =
   end (Environ.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
-      if is_dependent then Int.Map.add e None acc else acc
+      if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
       let subevars = evars_of_term b in
       (* evars appearing in the definition of an evar [e] are marked
@@ -518,14 +518,14 @@ let process_dependent_evar q acc evm is_dependent e =
          non-dependent goal, then, unless they are reach from another
          path, these evars are just other non-dependent goals. *)
       queue_set q is_dependent subevars;
-      if is_dependent then Int.Map.add e (Some subevars) acc else acc
+      if is_dependent then Evar.Map.add e (Some subevars) acc else acc
 
 let gather_dependent_evars q evm =
-  let acc = ref Int.Map.empty in
+  let acc = ref Evar.Map.empty in
   while not (Queue.is_empty q) do
     let (is_dependent,e) = Queue.pop q in
     (* checks if [e] has already been added to [!acc] *)
-    begin if not (Int.Map.mem e !acc) then
+    begin if not (Evar.Map.mem e !acc) then
         acc := process_dependent_evar q !acc evm is_dependent e  
     end
   done;
@@ -541,15 +541,15 @@ let gather_dependent_evars evm l =
 let evars_of_named_context nc =
   List.fold_right (fun (_, b, t) s ->
     Option.fold_left (fun s t ->
-      Int.Set.union s (evars_of_term t))
-      (Int.Set.union s (evars_of_term t)) b)
-    nc Int.Set.empty
+      Evar.Set.union s (evars_of_term t))
+      (Evar.Set.union s (evars_of_term t)) b)
+    nc Evar.Set.empty
 
 let evars_of_evar_info evi =
-  Int.Set.union (evars_of_term evi.evar_concl)
-    (Int.Set.union
+  Evar.Set.union (evars_of_term evi.evar_concl)
+    (Evar.Set.union
 	(match evi.evar_body with
-	| Evar_empty -> Int.Set.empty
+	| Evar_empty -> Evar.Set.empty
 	| Evar_defined b -> evars_of_term b)
 	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
 
@@ -564,25 +564,25 @@ let undefined_evars_of_term evd t =
       | Evar (n, l) ->
 	let acc = Array.fold_left evrec acc l in
 	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Int.Set.add n acc
+	  | Evar_empty -> Evar.Set.add n acc
 	  | Evar_defined c -> evrec acc c
 	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
       | _ -> fold_constr evrec acc c
   in
-  evrec Int.Set.empty t
+  evrec Evar.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
   List.fold_right (fun (_, b, t) s ->
     Option.fold_left (fun s t ->
-      Int.Set.union s (undefined_evars_of_term evd t))
-      (Int.Set.union s (undefined_evars_of_term evd t)) b)
-    nc Int.Set.empty
+      Evar.Set.union s (undefined_evars_of_term evd t))
+      (Evar.Set.union s (undefined_evars_of_term evd t)) b)
+    nc Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Int.Set.union (undefined_evars_of_term evd evi.evar_concl)
-    (Int.Set.union
+  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+    (Evar.Set.union
        (match evi.evar_body with
-	 | Evar_empty -> Int.Set.empty
+	 | Evar_empty -> Evar.Set.empty
 	 | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 0d482e9b0..d146bca47 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -66,7 +66,7 @@ val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
    returns the evar_map extended with dependent evars *)
 val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
 
-val non_instantiated : evar_map -> evar_info ExistentialMap.t
+val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** {6 Unification utils} *)
 
@@ -98,10 +98,10 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
     contained in the object, including defined evars *)
 
 
-val evars_of_term : constr -> Int.Set.t
+val evars_of_term : constr -> Evar.Set.t
 
-val evars_of_named_context : named_context -> Int.Set.t
-val evars_of_evar_info : evar_info -> Int.Set.t
+val evars_of_named_context : named_context -> Evar.Set.t
+val evars_of_evar_info : evar_info -> Evar.Set.t
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
     as dependent_evars and goals (these may overlap). A goal is an
@@ -112,16 +112,16 @@ val evars_of_evar_info : evar_info -> Int.Set.t
     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 -> (Int.Set.t option) Int.Map.t
+val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
 
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> constr -> Int.Set.t
-val undefined_evars_of_named_context : evar_map -> named_context -> Int.Set.t
-val undefined_evars_of_evar_info : evar_map -> evar_info -> Int.Set.t
+val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t
+val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** {6 Value/Type constraints} *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cebce3abe..1aa899771 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -27,8 +27,7 @@ module Store = Store.Make(Dummy)
 
 type evar = Term.existential_key
 
-let string_of_existential evk = "?" ^ string_of_int evk
-let existential_of_int evk = evk
+let string_of_existential evk = "?" ^ string_of_int (Evar.repr evk)
 
 type evar_body =
   | Evar_empty
@@ -81,15 +80,12 @@ let eq_evar_info ei1 ei2 =
     (** ppedrot: [eq_constr] may be a bit too permissive here *)
 
 (* spiwack: Revised hierarchy :
-   - ExistentialMap ( Maps of existential_keys )
-   - EvarInfoMap ( .t = evar_info ExistentialMap.t * evar_info ExistentialMap )
+   - Evar.Map ( Maps of existential_keys )
+   - EvarInfoMap ( .t = evar_info Evar.Map.t * evar_info Evar.Map )
    - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
    - evar_map (exported)
 *)
 
-module ExistentialMap = Int.Map
-module ExistentialSet = Int.Set
-
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
 
@@ -195,70 +191,70 @@ let metamap_to_list m =
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * Environ.env * constr * constr
 
+module EvMap = Evar.Map
+
 type evar_map = {
-  defn_evars : evar_info ExistentialMap.t;
-  undf_evars : evar_info ExistentialMap.t;
+  defn_evars : evar_info EvMap.t;
+  undf_evars : evar_info EvMap.t;
   universes  : Univ.UniverseLSet.t;
   univ_cstrs : Univ.universes;
   conv_pbs   : evar_constraint list;
-  last_mods  : ExistentialSet.t;
+  last_mods  : Evar.Set.t;
   metas      : clbinding Metamap.t
 }
 
-module ExMap = ExistentialMap
-
 (*** Lifting primitive from EvarMap. ***)
 
 (* HH: The progress tactical now uses this function. *)
 let progress_evar_map d1 d2 =
   let is_new k v =
     assert (v.evar_body == Evar_empty);
-    ExMap.mem k d2.defn_evars
+    EvMap.mem k d2.defn_evars
   in
-  not (d1 == d2) && ExMap.exists is_new d1.undf_evars
+  not (d1 == d2) && EvMap.exists is_new d1.undf_evars
 
 let add d e i = match i.evar_body with
 | Evar_empty ->
-  { d with undf_evars = ExMap.add e i d.undf_evars; }
+  { d with undf_evars = EvMap.add e i d.undf_evars; }
 | Evar_defined _ ->
-  { d with defn_evars = ExMap.add e i d.defn_evars; }
+  { d with defn_evars = EvMap.add e i d.defn_evars; }
 
 let remove d e =
-  let undf_evars = ExMap.remove e d.undf_evars in
-  let defn_evars = ExMap.remove e d.defn_evars in
+  let undf_evars = EvMap.remove e d.undf_evars in
+  let defn_evars = EvMap.remove e d.defn_evars in
   { d with undf_evars; defn_evars; }
 
 let find d e =
-  try ExMap.find e d.undf_evars
-  with Not_found -> ExMap.find e d.defn_evars
+  try EvMap.find e d.undf_evars
+  with Not_found -> EvMap.find e d.defn_evars
 
-let find_undefined d e = ExMap.find e d.undf_evars
+let find_undefined d e = EvMap.find e d.undf_evars
 
-let mem d e = ExMap.mem e d.undf_evars || ExMap.mem e d.defn_evars
+let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
 
 (* spiwack: this function loses information from the original evar_map
    it might be an idea not to export it. *)
 let to_list d =
   (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
   let l = ref [] in
-  ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
-  ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
+  EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
+  EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
   !l
 
 let undefined_map d = d.undf_evars
 
 let defined_map d = d.defn_evars
 
-let undefined_evars d = { d with defn_evars = ExMap.empty }
+let undefined_evars d = { d with defn_evars = EvMap.empty }
 
-let defined_evars d = { d with undf_evars = ExMap.empty }
+let defined_evars d = { d with undf_evars = EvMap.empty }
 
 (* spiwack: not clear what folding over an evar_map, for now we shall
     simply fold over the inner evar_map. *)
 let fold f d a =
-  ExMap.fold f d.defn_evars (ExMap.fold f d.undf_evars a)
+  EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a)
 
-let fold_undefined f d a = ExMap.fold f d.undf_evars a
+let fold_undefined f d a = EvMap.fold f d.undf_evars a
 
 let raw_map f d =
   let f evk info =
@@ -271,8 +267,8 @@ let raw_map f d =
     in
     ans
   in
-  let defn_evars = ExMap.mapi f d.defn_evars in
-  let undf_evars = ExMap.mapi f d.undf_evars in
+  let defn_evars = EvMap.mapi f d.defn_evars in
+  let undf_evars = EvMap.mapi f d.undf_evars in
   { d with defn_evars; undf_evars; }
 
 let raw_map_undefined f d =
@@ -285,13 +281,13 @@ let raw_map_undefined f d =
     in
     ans
   in
-  { d with undf_evars = ExMap.mapi f d.undf_evars; }
+  { d with undf_evars = EvMap.mapi f d.undf_evars; }
 
 let is_evar = mem
 
-let is_defined d e = ExMap.mem e d.defn_evars
+let is_defined d e = EvMap.mem e d.defn_evars
 
-let is_undefined d e = ExMap.mem e d.undf_evars
+let is_undefined d e = EvMap.mem e d.undf_evars
 
 let existential_value d (n, args) =
   let info = find d n in
@@ -321,8 +317,8 @@ let add_constraints d cstrs =
 
 (* evar_map are considered empty disregarding histories *)
 let is_empty d =
-  ExMap.is_empty d.defn_evars &&
-  ExMap.is_empty d.undf_evars &&
+  EvMap.is_empty d.defn_evars &&
+  EvMap.is_empty d.undf_evars &&
   List.is_empty d.conv_pbs &&
   Metamap.is_empty d.metas
 
@@ -343,31 +339,31 @@ let subst_evar_defs_light sub evd =
   assert (match evd.conv_pbs with [] -> true | _ -> false);
   let map_info i = subst_evar_info sub i in
   { evd with
-    undf_evars = ExMap.map map_info evd.undf_evars;
-    defn_evars = ExMap.map map_info evd.defn_evars;
+    undf_evars = EvMap.map map_info evd.undf_evars;
+    defn_evars = EvMap.map map_info evd.defn_evars;
     metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; }
 
 let subst_evar_map = subst_evar_defs_light
 
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
-  conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
+  conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
 (* spiwack: tentatively deprecated *)
 let create_goal_evar_defs sigma = { sigma with
-   (* conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } *)
+   (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *)
   metas=Metamap.empty } 
 
 let empty = {
-  defn_evars = ExMap.empty;
-  undf_evars = ExMap.empty;
+  defn_evars = EvMap.empty;
+  undf_evars = EvMap.empty;
   universes  = Univ.UniverseLSet.empty;
   univ_cstrs = Univ.initial_universes;
   conv_pbs   = [];
-  last_mods  = ExistentialSet.empty;
+  last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
 }
 
-let has_undefined evd = not (ExMap.is_empty evd.undf_evars)
+let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
 let evars_reset_evd ?(with_conv_pbs=false) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
@@ -382,23 +378,23 @@ let evar_source evk d = (find d evk).evar_source
 
 let define_aux def undef evk body =
   let oldinfo =
-    try ExMap.find evk undef
+    try EvMap.find evk undef
     with Not_found ->
-      if ExMap.mem evk def then
+      if EvMap.mem evk def then
         anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice")
       else
         anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar")
   in
   let () = assert (oldinfo.evar_body == Evar_empty) in
   let newinfo = { oldinfo with evar_body = Evar_defined body } in
-  ExMap.add evk newinfo def, ExMap.remove evk undef
+  EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
 let define evk body evd =
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
-  | _ -> ExistentialSet.add evk evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods
   in
   { evd with defn_evars; undf_evars; last_mods; }
 
@@ -419,7 +415,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter
     evar_candidates = candidates;
     evar_extra = Store.empty; }
   in
-  { evd with undf_evars = ExMap.add evk evar_info evd.undf_evars; }
+  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; }
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
@@ -434,7 +430,7 @@ let extract_conv_pbs evd p =
       ([],[])
       evd.conv_pbs
   in
-  {evd with conv_pbs = pbs1; last_mods = ExistentialSet.empty},
+  {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty},
   pbs
 
 let extract_changed_conv_pbs evd p =
@@ -461,10 +457,10 @@ let evar_list evd c =
 let collect_evars c =
   let rec collrec acc c =
     match kind_of_term c with
-      | Evar (evk,_) -> ExistentialSet.add evk acc
+      | Evar (evk,_) -> Evar.Set.add evk acc
       | _       -> fold_constr collrec acc c
   in
-  collrec ExistentialSet.empty c
+  collrec Evar.Set.empty c
 
 (**********************************************************)
 (* Sort variables *)
@@ -763,46 +759,46 @@ let compute_evar_dependency_graph (sigma : evar_map) =
   let fold evk evi acc =
     let fold_ev evk' acc =
       let tab =
-        try ExMap.find evk' acc
-        with Not_found -> ExistentialSet.empty
+        try EvMap.find evk' acc
+        with Not_found -> Evar.Set.empty
       in
-      ExMap.add evk' (ExistentialSet.add evk tab) acc
+      EvMap.add evk' (Evar.Set.add evk tab) acc
     in
     match evar_body evi with
     | Evar_empty -> assert false
-    | Evar_defined c -> ExistentialSet.fold fold_ev (collect_evars c) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (collect_evars c) acc
   in
-  ExMap.fold fold sigma.defn_evars ExMap.empty
+  EvMap.fold fold sigma.defn_evars EvMap.empty
 
 let evar_dependency_closure n sigma =
   (** Create the DAG of depth [n] representing the recursive dependencies of
       undefined evars. *)
   let graph = compute_evar_dependency_graph sigma in
   let rec aux n curr accu =
-    if Int.equal n 0 then ExistentialSet.union curr accu
+    if Int.equal n 0 then Evar.Set.union curr accu
     else
       let fold evk accu =
         try
-          let deps = ExMap.find evk graph in
-          ExistentialSet.union deps accu
+          let deps = EvMap.find evk graph in
+          Evar.Set.union deps accu
         with Not_found -> accu
       in
       (** Consider only the newly added evars *)
-      let ncurr = ExistentialSet.fold fold curr ExistentialSet.empty in
+      let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
       (** Merge the others *)
-      let accu = ExistentialSet.union curr accu in
+      let accu = Evar.Set.union curr accu in
       aux (n - 1) ncurr accu
   in
-  let undef = ExMap.domain (undefined_map sigma) in
-  aux n undef ExistentialSet.empty
+  let undef = EvMap.domain (undefined_map sigma) in
+  aux n undef Evar.Set.empty
 
 let evar_dependency_closure n sigma =
   let deps = evar_dependency_closure n sigma in
-  let map = ExMap.bind (fun ev -> find sigma ev) deps in
-  ExMap.bindings map
+  let map = EvMap.bind (fun ev -> find sigma ev) deps in
+  EvMap.bindings map
 
 let has_no_evar sigma =
-  ExMap.is_empty sigma.defn_evars && ExMap.is_empty sigma.undf_evars
+  EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
 let pr_evar_map_t depth sigma =
   let { universes = uvs; univ_cstrs = univs; } = sigma in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0beb46571..3d796d423 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -34,11 +34,6 @@ type evar = existential_key
 (** Existential variables. TODO: Should be made opaque one day. *)
 
 val string_of_existential : evar -> string
-val existential_of_int : int -> evar
-
-module ExistentialSet : Set.S with type elt = existential_key
-module ExistentialMap : Map.ExtS
-  with type key = existential_key and module Set := ExistentialSet
 
 (** {6 Evar infos} *)
 
@@ -157,10 +152,10 @@ val is_undefined : evar_map -> evar -> bool
 val add_constraints : evar_map -> Univ.constraints -> evar_map
 (** Add universe constraints in an evar map. *)
 
-val undefined_map : evar_map -> evar_info ExistentialMap.t
+val undefined_map : evar_map -> evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val defined_map : evar_map -> evar_info ExistentialMap.t
+val defined_map : evar_map -> evar_info Evar.Map.t
 (** Access the defined evar mapping directly. *)
 
 (** {6 Instantiating partial terms} *)
@@ -294,13 +289,13 @@ type evar_constraint = conv_pb * env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
-      (ExistentialSet.t -> evar_constraint -> bool) ->
+      (Evar.Set.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
 
 val evar_list : evar_map -> constr -> existential list
-val collect_evars : constr -> ExistentialSet.t
+val collect_evars : constr -> Evar.Set.t
 
 (** Metas *)
 val meta_list : evar_map -> (metavariable * clbinding) list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3623828f4..b80484599 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -32,7 +32,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PRef r1, PRef r2 -> eq_gr r1 r2
 | PVar v1, PVar v2 -> Id.equal v1 v2
 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
-  Int.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
+  Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
 | PRel i1, PRel i2 ->
   Int.equal i1 i2
 | PApp (t1, arg1), PApp (t2, arg2) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3fe2bbc12..c7c869d63 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -80,7 +80,7 @@ let evaluable_reference_eq r1 r2 = match r1, r2 with
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
-  Int.equal e1 e2 && Array.equal eq_constr ctx1 ctx2
+  Evar.equal e1 e2 && Array.equal eq_constr ctx1 ctx2
 | _ -> false
 
 let mkEvalRef = function
@@ -358,7 +358,7 @@ let venv = val_of_named_context [(vfx, None, dummy); (vfun, None, dummy)]
    vfx (expanded fixpoint) or vfun (named function). *)
 let substl_with_function subst sigma constr =
   let evd = ref sigma in
-  let minargs = ref Int.Map.empty in
+  let minargs = ref Evar.Map.empty in
   let v = Array.of_list subst in
   let rec subst_total k c = match kind_of_term c with
   | Rel i when k < i ->
@@ -367,7 +367,7 @@ let substl_with_function subst sigma constr =
       | (fx, Some (min, ref)) ->
         let (sigma, evk) = Evarutil.new_pure_evar !evd venv dummy in
         evd := sigma;
-        minargs := Int.Map.add evk min !minargs;
+        minargs := Evar.Map.add evk min !minargs;
         lift k (mkEvar (evk, [|fx;ref|]))
       | (fx, None) -> lift k fx
     else mkRel (i - Array.length v)
@@ -387,8 +387,8 @@ let solve_arity_problem env sigma fxminargs c =
     let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app c' in
     match kind_of_term h with
-        Evar(i,_) when Int.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
-          let minargs = Int.Map.find i fxminargs in
+        Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
+          let minargs = Evar.Map.find i fxminargs in
           if List.length rcargs < minargs then
             if strict then set_fix i
             else raise Partial;
@@ -415,7 +415,7 @@ let substl_checking_arity env subst sigma c =
      the other ones are replaced by the function symbol *)
   let rec nf_fix c =
     match kind_of_term c with
-        Evar(i,[|fx;f|] as ev) when Int.Map.mem i minargs ->
+        Evar(i,[|fx;f|] as ev) when Evar.Map.mem i minargs ->
           (match Evd.existential_opt_value sigma' ev with
               Some c' -> c'
             | None -> f)
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 27efb9a5d..225823411 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -211,7 +211,7 @@ struct
 
   let pat_of_constr c : term_pattern =
     (** To each evar we associate a unique identifier. *)
-    let metas = ref Evd.ExistentialMap.empty in
+    let metas = ref Evar.Map.empty in
     let rec pat_of_constr c = match kind_of_term c with
     | Rel _          -> Term DRel
     | Sort _         -> Term DSort
@@ -222,10 +222,10 @@ struct
     | Term.Meta _    -> assert false
     | Evar (i,_)     ->
       let meta =
-        try Evd.ExistentialMap.find i !metas
+        try Evar.Map.find i !metas
         with Not_found ->
           let meta = fresh_meta () in
-          let () = metas := Evd.ExistentialMap.add i meta !metas in
+          let () = metas := Evar.Map.add i meta !metas in
           meta
       in
       Meta meta
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9d57e1c80..81270b5f7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -60,7 +60,7 @@ let rec pr_constr c = match kind_of_term c with
       (str"(" ++ pr_constr c ++ spc() ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
   | Evar (e,l) -> hov 1
-      (str"Evar#" ++ int e ++ str"{" ++
+      (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const c -> str"Cst(" ++ pr_con c ++ str")"
   | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")"
@@ -516,7 +516,7 @@ let occur_meta_or_existential c =
 
 let occur_evar n c =
   let rec occur_rec c = match kind_of_term c with
-    | Evar (sp,_) when Int.equal sp n -> raise Occur
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | _ -> iter_constr occur_rec c
   in
   try occur_rec c; false with Occur -> true
@@ -912,18 +912,18 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (rel_context*constr) Int.Map.t
+type subst = (rel_context*constr) Evar.Map.t
 
 exception CannotFilter
 
 let filtering env cv_pb c1 c2 =
-  let evm = ref Int.Map.empty in
+  let evm = ref Evar.Map.empty in
   let define cv_pb e1 ev c1 =
-    try let (e2,c2) = Int.Map.find ev !evm in
+    try let (e2,c2) = Evar.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
     if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
     with Not_found ->
-      evm := Int.Map.add ev (e1,c1) !evm
+      evm := Evar.Map.add ev (e1,c1) !evm
   in
   let rec aux env cv_pb c1 c2 =
     match kind_of_term c1, kind_of_term c2 with
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 92a4d961a..1aa7d9e9e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -216,7 +216,7 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (rel_context*constr) Int.Map.t
+type subst = (rel_context*constr) Evar.Map.t
 val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 
 val decompose_prod_letin : constr -> int * rel_context * constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a1cb232ca..b5735bc64 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -506,7 +506,7 @@ let has_typeclasses filter evd =
   let check ev evi =
     filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi
   in
-  Evd.ExistentialMap.exists check (Evd.undefined_map evd)
+  Evar.Map.exists check (Evd.undefined_map evd)
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 14d6ad333..4f6741d87 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -228,7 +228,7 @@ type unify_flags = {
     (* This allows for instance to unify "forall x:A, B(x)" with "A' -> B'" *)
     (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *)
 
-  frozen_evars : ExistentialSet.t;
+  frozen_evars : Evar.Set.t;
     (* Evars of this set are considered axioms and never instantiated *)
     (* Useful e.g. for autorewrite *)
 
@@ -259,7 +259,7 @@ let default_unify_flags = {
   resolve_evars = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
+  frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;
   modulo_eta = true;
@@ -350,7 +350,7 @@ let use_full_betaiota flags =
   flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
 
 let isAllowedEvar flags c = match kind_of_term c with
-  | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
+  | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
   | _ -> false
 
 let check_compatibility env (sigma,metasubst,evarsubst) tyM tyN =
@@ -414,13 +414,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
 	| Evar (evk,_ as ev), _
-            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+            when not (Evar.Set.mem evk flags.frozen_evars) ->
 	    let cmvars = free_rels cM and cnvars = free_rels cN in
 	      if Int.Set.subset cnvars cmvars then
 		sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Evar (evk,_ as ev)
-            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+            when not (Evar.Set.mem evk flags.frozen_evars) ->
 	    let cmvars = free_rels cM and cnvars = free_rels cN in
 	      if Int.Set.subset cmvars cnvars then
 		sigma,metasubst,((curenv,ev,cM)::evarsubst)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 6fbbc2c5f..5dd4587a0 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -20,7 +20,7 @@ type unify_flags = {
   resolve_evars : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
-  frozen_evars : ExistentialSet.t;
+  frozen_evars : Evar.Set.t;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
   modulo_eta : bool;