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.

1 files changed, 1 insertions, 0 deletions

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();