aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 ac463391b2..3c151fac9b 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