diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 18:29:40 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 18:29:40 +0000 |
commit | 33eea163c72c70eaa3bf76506c1d07a8cde911fd (patch) | |
tree | 69eb4394fc0eb748fa16609e86dbf941234157d8 /kernel/constr.ml | |
parent | 71a9b7f264721b8afe5081bb0e13bcf8759d8403 (diff) |
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
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index eba490dbd..8b7505aeb 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) -> |