diff options
| author | Maxime Dénès | 2018-02-07 18:58:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 09:55:10 +0100 |
| commit | c9f3a6cbe5c410256fe88580019f5c7183bab097 (patch) | |
| tree | 766ec5d728e14080066fec43b99a6928198629c3 /kernel/nativecode.mli | |
| 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/nativecode.mli')
0 files changed, 0 insertions, 0 deletions