From 6000ddffed48b804669a5eae9be7c536bf5e19c5 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@cs.harvard.edu>
Date: Wed, 2 Sep 2015 18:50:09 -0700
Subject: print universes when dumping bytecode.

---
 kernel/cbytecodes.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 940b5528d..891d95378 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) ->
-- 
cgit v1.2.3