Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Intern names bound in match patterns | 2017-03-23 | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions. |
![]() |
index : coq | |
the Coq proof assistant |
aboutsummaryrefslogtreecommitdiffhomepage |
Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Intern names bound in match patterns | 2017-03-23 | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345): Cannot use names bound in matches inside Ltac definitions. |