aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 02:40:52 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 02:40:52 +0000
commit9ebb5a9db7aca6c441f7fef1af89fff49742602f (patch)
treed5b053ecd1d1950854291c3536d152068c4c0d03 /contrib/extraction
parent41caeae1003a24dd623aabe2907940d3151f1151 (diff)
Oups
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3322 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/mlutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index ac463391b..3c151fac9 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -496,7 +496,7 @@ let gen_subst v d t =
| MLrel i as a ->
let i'= i-n in
if i' < 1 then a
- else if i' <= Array.length v then
+ else if i' < Array.length v then
ast_lift n v.(i')
else MLrel (i+d)
| a -> ast_map_lift subst n a