| Commit message (Expand) | Author | Age |
* | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin | 2003-03-29 |
* | notations <>, Assumption avec existentiel, replace term | mohring | 2003-03-28 |
* | 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-27 |
* | *** empty log message *** | barras | 2003-03-21 |
* | reparations suite a la nouvelle syntaxe: | barras | 2003-03-14 |
* | Ajout réaffichage SubClass | herbelin | 2003-03-13 |
* | *** empty log message *** | barras | 2003-03-12 |
* | Renommage indpar pour usage plus general | herbelin | 2003-03-12 |
* | Bug délimiteur de scope en vieil affichage ast | herbelin | 2003-03-04 |
* | Retour vieil afficheur | herbelin | 2003-03-03 |
* | 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-27 |
* | Affinement entree annot | herbelin | 2003-02-17 |
* | Debugger plus informatif | delahaye | 2003-02-13 |
* | Ajout du traducteur | desmettr | 2003-02-05 |
* | Pour satisfaire ProofGeneral | coq | 2003-01-31 |
* | Adds a possibility to construct a term as if it had been parsed through | bertot | 2003-01-30 |
* | Deux p\'tits trucs ;) | coq | 2003-01-27 |
* | I changed the interface to make sure SearchAbout is defined according to | bertot | 2003-01-22 |
* | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin | 2003-01-19 |
* | Rétablissement pr_pattern | herbelin | 2003-01-19 |
* | Bugs affichage | herbelin | 2003-01-16 |
* | 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-15 |
* | Export M + Module M <: SIG | coq | 2003-01-09 |
* | Retour printer ast pour V7.4 | herbelin | 2003-01-07 |
* | SearchAbout | filliatr | 2003-01-06 |
* | Prise en compte notations dans les extensions de motiff | herbelin | 2002-12-28 |
* | 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-21 |
* | Petit netoyage dans lib | coq | 2002-12-19 |
* | bug: Global.env() executé au chargement -> eta-expansion | letouzey | 2002-12-19 |
* | 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-15 |
* | possibilité de faire Print M avec M module ou modtype au lieu de Print Modul... | letouzey | 2002-12-13 |
* | Ajout du vernac Proof with | gregoire | 2002-12-12 |
* | Bugs divers | herbelin | 2002-12-10 |
* | Ajout options -v7 et -v8, et commandes V7only et V8only | herbelin | 2002-12-10 |
* | Problèmes et améliorations affichage; Changement Simpl | herbelin | 2002-12-09 |
* | Ajout Simpl et Change sur des sous-termes | herbelin | 2002-12-09 |
* | Correction divers bugs d'affichage; explicitation du niveau de grammaire quan... | herbelin | 2002-12-04 |
* | Modification Require From | mohring | 2002-12-04 |
* | la table PARAMETER n'existe plus (mergé dans la table CONSTANT) | letouzey | 2002-12-03 |