From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 28 Oct 2015 11:16:24 +0100
Subject: Refine Gregory Malecha's patch on VM and universe polymorphism.

- Universes are now represented in the VM by a structured constant containing the
  global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
  a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
  constructor arguments, which has to be prevented.
  Was showing up for instance when evaluating [cons _ list (nil _)] with
  a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
  Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.

Patch written with Benjamin Grégoire.
---
 dev/vm_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 272df7b421..1c501df808 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -79,6 +79,7 @@ and ppwhd whd =
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
+  | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl)
 
 and ppvblock b =
   open_hbox();
-- 
cgit v1.2.3