| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-26 | Fix #11039: proof of False with template poly and nonlinear universes | Gaëtan Gilbert | |
| Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |