From c9f3a6cbe5c410256fe88580019f5c7183bab097 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 7 Feb 2018 18:58:16 +0100
Subject: Fix #6677: Critical bug with VM and universes

This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.
---
 dev/vm_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index f819d2e6a9..b410d017d0 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,7 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Atype u -> print_string "Type(...)"
+  | Atype (u,l) -> print_string "Type(...)"
   | Aind(sp,i) ->  print_string "Ind(";
       print_string (MutInd.to_string sp);
       print_string ","; print_int i;
-- 
cgit v1.2.3