diff options
| author | Pierre-Marie Pédrot | 2015-09-06 13:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-06 13:23:28 +0200 |
| commit | d8b245d688ff64d17acd9e7591daf6d63b4e54f7 (patch) | |
| tree | 0e202d1f39e97844d94a873b30e4fb14fb481f84 /kernel/cbytecodes.ml | |
| parent | c53f2f75375dfffd2f258c76f5b722d37ab0daf9 (diff) | |
| parent | 5080991902a05ee720ab1d6fa1c9d592d3ffd36c (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 940b5528d3..891d95378b 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -207,7 +207,8 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,_u) -> str "getglobal " ++ pr_con id + | Kgetglobal (id,u) -> + str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> |