| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot |
| 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 |