| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | A new step on using alpha-conversion in printing notations. |  Hugo Herbelin | 2016-07-18 |
| | | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns). | ||
| * | Fixing #4932 (anomaly when using binders as terms in recursive notations). | Hugo Herbelin | 2016-07-17 |
| This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |