| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-01-11 | Add a test for a weird behaviour of tactic matching. | Pierre-Marie Pédrot | |
| The arity of a destructuring let in a pattern is allowed to be shorter than the case term node it actually matches. This is an unexpected side-effect of the legacy expanded representation of cases that happens to be relied upon in the wild, as evidenced by the CI failures from #13723. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |