Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Properly handling polymorphic inductive subtyping in the kernel. | 2017-07-11 | |
Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming. |