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.
---
 kernel/cbytecodes.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index b13b0607b3..0a24a75d68 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -19,6 +19,7 @@ type tag = int
 
 let accu_tag = 0
 
+let type_atom_tag = 2
 let max_atom_tag = 2
 let proj_tag = 3
 let fix_app_tag = 4
-- 
cgit v1.2.3