| Commit message (Expand) | Author | Age |
* | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin | 2003-11-01 |
* | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin | 2003-10-30 |
* | Ordre (symbolique) des Require | herbelin | 2003-10-28 |
* | Passage de la notations de paire dans core_scope | herbelin | 2003-10-28 |
* | Passage des notations de type dans type_scope | herbelin | 2003-10-28 |
* | Ajout %core; MAJ niveau connecteurs logique | herbelin | 2003-10-28 |
* | Commentaires | herbelin | 2003-10-23 |
* | reorganisation des niveaux (ex: = est a 70) | barras | 2003-10-22 |
* | Maintenant avant Datatypes | herbelin | 2003-10-21 |
* | ajouts | herbelin | 2003-10-21 |
* | Des implicites plus 'naturels' pour eq_ind, identity_ind and co | herbelin | 2003-10-17 |
* | nouvelle syntaxe de ltac | barras | 2003-10-16 |
* | Changement 'as notation' en 'where notation' | herbelin | 2003-10-14 |
* | Argument de except, error implicite seulement en v8; Changement 'as notation'... | herbelin | 2003-10-14 |
* | Argument de None implicite seulement en v8 | herbelin | 2003-10-14 |
* | Argument implicite pour None, error, except | herbelin | 2003-10-13 |
* | Enregistrement '^' en v8 | herbelin | 2003-10-13 |
* | mise a jour nouvelle syntaxe | barras | 2003-10-11 |
* | nat_scope ouvert par defaut | herbelin | 2003-10-10 |
* | identity est equivalent sur Type (sauf sans argument) | herbelin | 2003-10-10 |
* | type_scope | herbelin | 2003-10-10 |
* | Suppression de definitions equivalentes | herbelin | 2003-10-10 |
* | Delimiters N devient 'nat' | herbelin | 2003-10-10 |
* | changement nouvelle syntaxe (pt fixes) | barras | 2003-10-10 |
* | Cacher les .v8 | herbelin | 2003-10-03 |
* | well_founded_induction de nouveau transparent | letouzey | 2003-09-28 |
* | Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type... | herbelin | 2003-09-23 |
* | traducteur: affiche les commentaires a l'interieur des commandes | barras | 2003-09-22 |
* | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin | 2003-09-21 |
* | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin | 2003-09-21 |
* | Nettoyage | herbelin | 2003-09-21 |
* | Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem... | herbelin | 2003-09-19 |
* | Suppression DatatypesSyntax et PeanoSyntax qui était vides | herbelin | 2003-09-12 |
* | Bind et Delimit pour nat | herbelin | 2003-09-12 |
* | Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ... | herbelin | 2003-09-11 |
* | Affichage {}+{}, niveau paire au plus haut | herbelin | 2003-08-10 |
* | recursion bien fondee sur des pairs | filliatr | 2003-07-08 |
* | Suppression d'une occurrence superflue d'argument de type dans Notation sacha... | herbelin | 2003-06-10 |
* | Deplacement delimiteur T dans Notations | herbelin | 2003-06-10 |
* | Bug niveau | herbelin | 2003-05-29 |
* | Ne pas mettre d'associatif a droite au niveau 3 en V7 | herbelin | 2003-05-29 |
* | 'only parsing' pour le passage de trucT a truc | herbelin | 2003-05-27 |
* | V8Notation | herbelin | 2003-05-22 |
* | Ajout V8Notation | herbelin | 2003-05-22 |
* | Concentration des notations officielles dans Init/Notations; restructuration ... | herbelin | 2003-05-21 |
* | Blancs | herbelin | 2003-04-29 |
* | Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot | letouzey | 2003-04-28 |
* | Intégration DatatypesSyntax à Datatypes | herbelin | 2003-04-17 |
* | Intégration DatatypesSyntax à Datatypes | herbelin | 2003-04-17 |
* | Syntaxe 'x=y:>T' | herbelin | 2003-04-17 |