| Age | Commit message (Expand) | Author |
| 2003-03-29 | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin |
| 2003-03-28 | notations <>, Assumption avec existentiel, replace term | mohring |
| 2003-03-27 | MAJ des mots-clés, Definition, Theorem, ... | herbelin |
| 2003-03-27 | MAJ des mots-clés, Definition, Theorem, ... | herbelin |
| 2003-03-27 | Affinement nommage des productions | herbelin |
| 2003-03-21 | *** empty log message *** | barras |
| 2003-03-14 | reparations suite a la nouvelle syntaxe: | barras |
| 2003-03-13 | Ajout réaffichage SubClass | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-03-12 | Renommage indpar pour usage plus general | herbelin |
| 2003-03-04 | Bug délimiteur de scope en vieil affichage ast | herbelin |
| 2003-03-03 | Retour vieil afficheur | herbelin |
| 2003-02-27 | Interpretation des entiers dans les reels via les scopes | desmettr |
| 2003-02-27 | Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'... | herbelin |
| 2003-02-27 | Correction test token normal | herbelin |
| 2003-02-27 | Le lexeur et Notation savent reconnaître si un unicode des blocs | herbelin |
| 2003-02-27 | Retour nouvel afficheur | herbelin |
| 2003-02-17 | Affinement entree annot | herbelin |
| 2003-02-13 | Debugger plus informatif | delahaye |
| 2003-02-05 | Ajout du traducteur | desmettr |
| 2003-01-31 | Pour satisfaire ProofGeneral | coq |
| 2003-01-30 | Adds a possibility to construct a term as if it had been parsed through | bertot |
| 2003-01-27 | Deux p\'tits trucs ;) | coq |
| 2003-01-22 | I changed the interface to make sure SearchAbout is defined according to | bertot |
| 2003-01-19 | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin |
| 2003-01-19 | Rétablissement pr_pattern | herbelin |
| 2003-01-16 | Bugs affichage | herbelin |
| 2003-01-15 | Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un... | herbelin |
| 2003-01-15 | Nouvelle interprétation des nombres réels | desmettr |
| 2003-01-09 | Export M + Module M <: SIG | coq |
| 2003-01-07 | Retour printer ast pour V7.4 | herbelin |
| 2003-01-06 | SearchAbout | filliatr |
| 2002-12-28 | Prise en compte notations dans les extensions de motiff | herbelin |
| 2002-12-21 | Légère amélioration des messages d'erreur des with-bindings et des Rewrite | herbelin |
| 2002-12-21 | Affinement affichage | herbelin |
| 2002-12-21 | Plus de notation cablees dans 'annot' | herbelin |
| 2002-12-19 | Petit netoyage dans lib | coq |
| 2002-12-19 | bug: Global.env() executé au chargement -> eta-expansion | letouzey |
| 2002-12-15 | Meilleure factorisation des entrées NEXT internes | herbelin |
| 2002-12-15 | Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxe | herbelin |
| 2002-12-15 | Pas de 0 dans positive | herbelin |
| 2002-12-13 | possibilité de faire Print M avec M module ou modtype au lieu de Print Modul... | letouzey |
| 2002-12-12 | Ajout du vernac Proof with | gregoire |
| 2002-12-10 | Bugs divers | herbelin |
| 2002-12-10 | Ajout options -v7 et -v8, et commandes V7only et V8only | herbelin |
| 2002-12-09 | Problèmes et améliorations affichage; Changement Simpl | herbelin |
| 2002-12-09 | Ajout Simpl et Change sur des sous-termes | herbelin |
| 2002-12-04 | Correction divers bugs d'affichage; explicitation du niveau de grammaire quan... | herbelin |
| 2002-12-04 | Modification Require From | mohring |
| 2002-12-03 | la table PARAMETER n'existe plus (mergé dans la table CONSTANT) | letouzey |