From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 dev/vm_printers.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'dev/vm_printers.ml')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 802b0f9d80..272df7b421 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -13,7 +13,7 @@ let ppripos (ri,pos) =
 	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
-  | Reloc_getglobal (kn,_) ->
+  | Reloc_getglobal kn ->
       print_string ("getglob "^(string_of_con kn)^"\n"));
    print_flush ()
 
@@ -30,7 +30,7 @@ let ppsort = function
 
 let print_idkey idk =
   match idk with
-  | ConstKey (sp,_) ->
+  | ConstKey sp ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
@@ -61,7 +61,8 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aind((sp,i),_) ->  print_string "Ind(";
+  | Atype u -> print_string "Type(...)"
+  | Aind(sp,i) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"
-- 
cgit v1.2.3