Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Moving the [split] tactic out of the AST. | 2014-06-06 | |
* | Removing symmetry from the atomic tactics. | 2014-06-02 | |
* | Allowing Ltac definitions that may be unusable because of a built-in | 2014-05-21 | |
* | Moving left & right tactics out of the AST. | 2014-05-21 | |
* | Moving argument-free tactics out of the AST into a dedicated | 2014-05-16 | |
* | Now parsing rules of ML-declared tactics are only made available after the | 2014-05-12 | |
* | Fix bug#2080: error message on Ltac name clash with primitive tactics | 2014-01-10 | |
* | Centralizing the Ltac-defining functions in Tacenv. | 2013-11-10 | |
* | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | 2013-11-10 | |
* | Revert the previous commit. It broke Coq compilation. | 2013-11-09 | |
* | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | 2013-11-09 |