I have some Universe Inconsistencies showing up when importing files from two libraries (
Because Holiday time is no time to deal with this hell, I innocently decided to postpone the pain of figuring out a solution by setting
Unset Universe Checking.
However when I do so, the following definition that usually goes through now fails:
Variant foo : Type -> Type := | Foo : unit -> foo unit.
With the error
Error: Ill-formed template inductive declaration: not polymorphic on any universe. (on
Is that expected? Is there a way to beg Coq to really forget about the Universes and let me keep going by any chance?
Unset Auto Template Polymorphism.
template poly is useless if you're in unset univ checking mode so it should be fine
Ah great, thanks Gaëtan!
looks like the kernel gets a different result than predicted by the higher layers because Evd.set_eq_sort (called from ComInductive.inductive_levels) does nothing when unset univ checking
Last updated: Jan 29 2023 at 06:02 UTC