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

6 files changed, 62 insertions, 6 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index eba490dbda..8b7505aebe 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -31,7 +31,7 @@ open Univ
 open Esubst
 
 
-type existential_key = int
+type existential_key = Evar.t
 type metavariable = int
 
 (* This defines the strategy to use for verifiying a Cast *)
@@ -341,7 +341,7 @@ let compare_head f t1 t2 =
   | App (c1,l1), App (c2,l2) ->
     Int.equal (Array.length l1) (Array.length l2) &&
       f c1 c2 && Array.equal f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
   | Const c1, Const c2 -> eq_constant c1 c2
   | Ind c1, Ind c2 -> eq_ind c1 c2
   | Construct c1, Construct c2 -> eq_constructor c1 c2
@@ -391,7 +391,7 @@ let constr_ord_int f t1 t2 =
     | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
     | Evar (e1,l1), Evar (e2,l2) ->
-        ((-) =? (Array.compare f)) e1 e2 l1 l2
+        (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
     | Const c1, Const c2 -> con_ord c1 c2
     | Ind ind1, Ind ind2 -> ind_ord ind1 ind2
     | Construct ct1, Construct ct2 -> constructor_ord ct1 ct2
@@ -469,7 +469,7 @@ let hasheq t1 t2 =
     | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
       n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
     | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2
-    | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 & array_eqeq l1 l2
     | Const c1, Const c2 -> c1 == c2
     | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2
     | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 59430125f7..261b6bfb4c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -9,7 +9,7 @@
 open Names
 
 (** {6 Existential variables } *)
-type existential_key = int
+type existential_key = Evar.t
 
 (** {6 Existential variables } *)
 type metavariable = int
diff --git a/kernel/evar.ml b/kernel/evar.ml
new file mode 100644
index 0000000000..d7e32626f5
--- /dev/null
+++ b/kernel/evar.ml
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type t = int
+
+let repr x = x
+let unsafe_of_int x = x
+let compare = Int.compare
+let equal = Int.equal
+
+module Self =
+struct
+  type _t = t
+  type t = _t
+  let compare = compare
+end
+
+module Set = Set.Make(Self)
+module Map = CMap.Make(Self)
diff --git a/kernel/evar.mli b/kernel/evar.mli
new file mode 100644
index 0000000000..8e8b88d942
--- /dev/null
+++ b/kernel/evar.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module defines existential variables, which are isomorphic to [int].
+    Nonetheless, casting from an [int] to a variable is deemed unsafe, so that
+    to keep track of such casts, one has to use the provided {!unsafe_of_int}
+    function. *)
+
+type t
+(** Type of existential variables. *)
+
+val repr : t -> int
+(** Recover the underlying integer. *)
+
+val unsafe_of_int : int -> t
+(** This is not for dummies. Do not use this function if you don't know what you
+    are doing. *)
+
+val equal : t -> t -> bool
+(** Equality over existential variables. *)
+
+val compare : t -> t -> int
+(** Comparison over existential variables. *)
+
+module Set : Set.S with type elt = t
+module Map : CMap.ExtS with type key = t and module Set := Set
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 36b3d83237..cbc147e9e5 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -2,6 +2,7 @@ Names
 Univ
 Esubst
 Sorts
+Evar
 Constr
 Context
 Vars
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1f5a6a6a0f..48c63ac96b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -277,7 +277,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
-        if Int.equal ev1 ev2 then
+        if Evar.equal ev1 ev2 then
           let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
           convert_vect l2r infos el1 el2
             (Array.map (mk_clos env1) args1)