diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 18:58:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 09:55:10 +0100 |
| commit | c9f3a6cbe5c410256fe88580019f5c7183bab097 (patch) | |
| tree | 766ec5d728e14080066fec43b99a6928198629c3 /kernel/cbytegen.ml | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
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.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5dab2932d..4a34dbcff 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont = of the structured constant, while the later (if any) will be applied as arguments. *) let open Univ in begin - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in + let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m - in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont + if List.is_empty s then + compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont else let compile_get_univ reloc idx sz cont = set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont + (Bstrconst (Const_type u)) (Array.of_list s) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz |