aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 7643fdb55f..ca24f9b689 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -284,7 +284,7 @@ let emit_instr env = function
if n <= 1 then out env (opSETFIELD0+n)
else (out env opSETFIELD;out_int env n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
- | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p
+ | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
(* spiwack *)
| Kbranch lbl -> out env opBRANCH; out_label env lbl