aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-14 10:26:19 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-14 10:26:19 +0000
commit32b768c62eada16d07453b63fd4bdabfebed0d05 (patch)
treec8c4dcab2d55bce94dfee7f88fa3753aca64b034 /lib
parent72a7fd50cba4ba45de9ec60a8fea6da5531ba7b8 (diff)
Bug PR#324
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4398 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml
index d6e160efd..4d86f04f5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -401,7 +401,7 @@ let array_tl v =
let array_last v =
match Array.length v with
- | 0 -> failwith "aray_last"
+ | 0 -> failwith "array_last"
| n -> v.(pred n)
let array_cons e v = Array.append [|e|] v