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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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/vm.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'kernel/vm.mli') diff --git a/kernel/vm.mli b/kernel/vm.mli index bc1978663..43a42eb9c 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity" val whd_val : values -> whd val uni_lvl_val : values -> Univ.universe_level -val instantiate_universe : Univ.universe -> stack -> Univ.universe (** Arguments *) -- cgit v1.2.3