| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-05-21 | Allowing Ltac definitions that may be unusable because of a built-in | Pierre-Marie Pédrot |
| 2014-05-21 | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-01-10 | Fix bug#2080: error message on Ltac name clash with primitive tactics | xclerc |
| 2013-11-10 | Centralizing the Ltac-defining functions in Tacenv. | ppedrot |
| 2013-11-10 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot |
| 2013-11-09 | Revert the previous commit. It broke Coq compilation. | ppedrot |
| 2013-11-09 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |