aboutsummaryrefslogtreecommitdiff
path: root/lib/cArray.ml
diff options
context:
space:
mode:
authorppedrot2012-11-13 22:38:16 +0000
committerppedrot2012-11-13 22:38:16 +0000
commit98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch)
treee7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /lib/cArray.ml
parent1d436a18f2f72b57ea09a6d27709a36b63be863a (diff)
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/cArray.ml')
-rw-r--r--lib/cArray.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 4615ad0388..a5e38534f3 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -102,7 +102,9 @@ let compare item_cmp v1 v2 =
cmp (Array.length v1 - 1)
let equal cmp t1 t2 =
- Array.length t1 = Array.length t2 &&
+ if t1 == t2 then true else
+ if not (Array.length t1 = Array.length t2) then false
+ else
let rec aux i =
(i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
in aux 0