| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-19 | Fix #11549: Ltac2 is incompatible with $. | Pierre-Marie Pédrot | |
| We use the same kind of trick as the one we used for &IDENT, namely check that no space appear between the dollar sign and the identifier. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |