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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/vm_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index f819d2e6a9..b410d017d0 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -61,7 +61,7 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Atype u -> print_string "Type(...)" + | Atype (u,l) -> print_string "Type(...)" | Aind(sp,i) -> print_string "Ind("; print_string (MutInd.to_string sp); print_string ","; print_int i; |