| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Compatibilité ocamlweb pour cible doc |  herbelin | 2005-01-21 |
| * | restructuration des printers: proofs passe avant parsing |  barras | 2004-09-17 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | name_app accessible a tous dans Nameops | herbelin | 2003-12-19 |
| * | Fonctions utiles | herbelin | 2003-09-23 |
| * | Déplacement traducteur de nom dans Constrextern pour accès aux noms longs | herbelin | 2003-06-10 |
| * | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin | 2003-05-19 |
| * | Mise en place d'un traducteur de noms v7->v8 | herbelin | 2003-03-31 |
| * | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin | 2003-03-29 |
| * | Petit netoyage dans lib |  coq | 2002-12-19 |
| * | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
| * | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
| * | reparation de Locate | barras | 2001-11-29 |
| * | nouvel algo de conversion plus uniforme | barras | 2001-11-29 |
| * | GROS COMMIT: | barras | 2001-11-05 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |