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 |