| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-10-28 | Fix #10903: type-in-type allows fixpoints on sprop inductives | Gaëtan Gilbert | |
| I still don't know why it produces a Not_found instead of a regular error in coqtop but let's forget about it. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |