diff options
| author | Maxime Dénès | 2015-07-06 17:04:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-06 17:04:10 +0200 |
| commit | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (patch) | |
| tree | a650355330521a776719279328e82a47527d15a5 /kernel/cemitcodes.ml | |
| parent | 7ad2fe2bd30a07eb2495ea8cf902a24ef13a3627 (diff) | |
| parent | 2face8d77628ded64f7d0a824f4b377694b9d7fd (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2535a64d3c..0d9334a50c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -225,6 +225,7 @@ let emit_instr = function if n <= 1 then out (opSETFIELD0+n) else (out opSETFIELD;out_int n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" + | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 |