| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... |  herbelin | 2003-01-19 |
| * | Ajout Simpl et Change sur des sous-termes | herbelin | 2002-12-09 |
| * | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
| * | Ajout d'un suffixe "as [ names ]" pour nommer manuellement les | herbelin | 2002-10-21 |
| * | NewDestruct/NewInduction acceptent l'option "using" | herbelin | 2002-10-21 |
| * | L'application de ltac attend une référence; meilleure protection contre | herbelin | 2002-10-14 |
| * | Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage | herbelin | 2002-10-13 |
| * | Modules dans COQ\!\!\!\! |  coq | 2002-08-02 |
| * | Fichier des expressions de tactiques | herbelin | 2002-05-29 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |