| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixes #7195 (missing freshness condition in Ltac pattern-matching names). |  Hugo Herbelin | 2018-04-08 |
| We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |