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

4 files changed, 11 insertions, 11 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7b1ccd542d..4260d5553b 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -101,7 +101,7 @@ let fail_quick_unif_flags = {
   resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  frozen_evars = ExistentialSet.empty;
+  frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index efed7f63de..36ba80202f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -18,9 +18,9 @@ open Evarsolve
 (******************************************)
 
 let depends_on_evar evk _ (pbty,_,t1,t2) =
-  try Int.equal (head_evar t1) evk
+  try Evar.equal (head_evar t1) evk
   with NoHeadEvar ->
-  try Int.equal (head_evar t2) evk
+  try Evar.equal (head_evar t2) evk
   with NoHeadEvar -> false
 
 let define_and_solve_constraints evk c evd =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 50541151ad..68eb1c5861 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -27,7 +27,7 @@ type goal = {
    whether we do want some tags displayed besides the goal or not. *)
 
 
-let pr_goal {content = e} = str "GOAL:" ++ Pp.int e
+let pr_goal {content = e} = str "GOAL:" ++ Pp.int (Evar.repr e)
 
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
@@ -41,14 +41,14 @@ let build e =
   }
 
 
-let uid {content = e} = string_of_int e
+let uid {content = e} = string_of_int (Evar.repr e)
 let get_by_uid u =
   (* this necessarily forget about tags.
      when tags are to be implemented, they
      should be done another way.
      We could use the store in evar_extra,
      for instance. *)
-  build (int_of_string u)
+  build (Evar.unsafe_of_int (int_of_string u))
 
 (* Builds a new goal with content evar [e] and
    inheriting from goal [gl]*)
@@ -184,7 +184,7 @@ module Refinable = struct
     | [] , _ -> l2
     | _ , [] -> l1
     | a::l1 , b::_ when a > b -> a::(fusion l1 l2)
-    | a::l1 , b::l2 when Int.equal a b -> a::(fusion l1 l2)
+    | a::l1 , b::l2 when Evar.equal a b -> a::(fusion l1 l2)
     | _ , b::l2 -> b::(fusion l1 l2)
 
   let update_handle handle init_defs post_defs =
@@ -359,7 +359,7 @@ let plus s1 s2 env rdefs goal info =
   with UndefinedHere -> s2 env rdefs goal info
 
 (* Equality of two goals *)
-let equal { content = e1 } { content = e2 } = Int.equal e1 e2
+let equal { content = e1 } { content = e2 } = Evar.equal e1 e2
 
 let here goal value _ _ goal' _ =
   if equal goal goal' then
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 843af1373b..9467d2d710 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -487,7 +487,7 @@ module V82 = struct
     let goals =
       List.map begin fun (e,_) ->
 	Goal.build e
-      end (Evd.ExistentialMap.bindings undef)
+      end (Evar.Map.bindings undef)
     in
     { pv with comb = goals }
       
@@ -504,14 +504,14 @@ module V82 = struct
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =
-      Int.Set.elements (Evarutil.evars_of_term c)
+      Evar.Set.elements (Evarutil.evars_of_term c)
     in
     List.flatten (List.map evars_of_initial initial)
 
   let instantiate_evar n com pv =
     let (evk,_) =
       let evl = Evarutil.non_instantiated pv.solution in
-      let evl = Evd.ExistentialMap.bindings evl in
+      let evl = Evar.Map.bindings evl in
       if (n <= 0) then
 	Errors.error "incorrect existential variable index"
       else if List.length evl < n then