From 33eea163c72c70eaa3bf76506c1d07a8cde911fd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 18 Sep 2013 18:29:40 +0000
Subject: 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
---
 kernel/constr.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/constr.ml')

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) ->
-- 
cgit v1.2.3