aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-12-11 13:02:37 +0100
committerPierre-Marie Pédrot2015-12-11 13:06:53 +0100
commit50d241267e2eb41cb06eb2f48a5ce440f0458b71 (patch)
treef5d7c15cd62cf41177f2f902559ff21fc2988c54 /kernel/cbytegen.ml
parente70165079e8defe490a568ece20a7029e4c1626e (diff)
parent119d61453c6761f20b8862f47334bfb8fae0049e (diff)
Merge branch 'v8.5'
Diffstat (limited to 'kernel/cbytegen.ml')
-rw-r--r--kernel/cbytegen.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 1f7cc3c7a6..67745d887b 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -175,7 +175,7 @@ let comp_env_cofix ndef arity rfv =
let push_param n sz r =
{ r with
nb_stack = r.nb_stack + n;
- in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack }
+ in_stack = add_param n sz r.in_stack }
(* [push_local sz r] add a new variable on the stack at position [sz] *)
let push_local sz r =