| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2016-07-18 | A new step on using alpha-conversion in printing notations. | Hugo Herbelin | |
| 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). | |||
| 2016-07-17 | Fixing #4932 (anomaly when using binders as terms in recursive notations). | Hugo Herbelin | |
| 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 formal proof system |
| aboutsummaryrefslogtreecommitdiff |