| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-19 | Addressing parsing part #13078. | Hugo Herbelin | |
| We don't give sense to pattern/binders in leftmost position. | |||
| 2020-10-19 | Fixing printing part of #13078 (anomaly with binding notations in patterns). | Hugo Herbelin | |
| We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |