| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Renaming goal-entering functions. |  Pierre-Marie Pédrot | 2014-09-06 |
| * | Reorganization of tactics: |  Hugo Herbelin | 2014-08-18 |
| * | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | This commit adds full universe polymorphism and fast projections to Coq. |  Matthieu Sozeau | 2014-05-06 |
| * | Removing tactic compatibility layer from Eqdecide. | Pierre-Marie Pédrot | 2014-03-27 |
| * | Adding an interface to Eqdecide and putting the grammar rules in a dedicated | Pierre-Marie Pédrot | 2014-03-26 |
| * | Fichiers tactics/*.ml4 remplacent les tactics/*.v |  herbelin | 2002-05-29 |
| * | petits changements cosmetiques sur les tactiques |  barras | 2002-02-15 |
| * | GROS COMMIT: | barras | 2001-11-05 |
| * | entetes |  filliatr | 2001-03-15 |
| * | Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)... | herbelin | 2001-02-14 |
| * | EqDecide | filliatr | 2001-02-06 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |