| Age | Commit message (Expand) | Author |
|---|---|---|
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot |
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin |
| 2014-08-31 | Getting rid of atomic tactics in Tacenv. | Pierre-Marie Pédrot |
| 2014-08-31 | Moving code of tactic interpretation from Tacenv to Vernacentries. | Pierre-Marie Pédrot |
| 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 |