| Age | Commit message (Expand) | Author |
|---|---|---|
| 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 |