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/csymtable.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/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2bbb867cd..bbd284bc1 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2 | Const_type _ , _ -> false let rec hash_structured_constant c = |