| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | TACTIC EXTEND now takes an optional level as argument. |  Maxime Dénès | 2017-02-24 |
| | | | | | | | | | | | | | | The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ... | ||
| * | Ltac as a plugin. |  Pierre-Marie Pédrot | 2017-02-17 |
| This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |