Mutual inductive incorrectly squashed without explicit : Prop
#17801
Labels
kind: regression
Problems that were not present in previous versions.
part: inductives
Inductive types, fixpoints, etc.
part: universes
The universe system.
NB: in 8.17 there is no issue as they both get put in Type.
Putting both in Prop could also be considered correct, but putting one in Prop but not the other is not correct.
The text was updated successfully, but these errors were encountered: