aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2003-10-14Changement 'as notation' en 'where notation'herbelin
2003-10-14Argument de except, error implicite seulement en v8; Changement 'as notation'...herbelin
2003-10-14Argument de None implicite seulement en v8herbelin
2003-10-13Argument implicite pour None, error, exceptherbelin
2003-10-13Enregistrement '^' en v8herbelin
2003-10-11mise a jour nouvelle syntaxebarras
2003-10-10nat_scope ouvert par defautherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10type_scopeherbelin
2003-10-10Suppression de definitions equivalentesherbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-03Cacher les .v8herbelin
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Nettoyageherbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
2003-09-12Bind et Delimit pour natherbelin
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
2003-08-10Affichage {}+{}, niveau paire au plus hautherbelin
2003-07-08recursion bien fondee sur des pairsfilliatr
2003-06-10Suppression d'une occurrence superflue d'argument de type dans Notation sacha...herbelin
2003-06-10Deplacement delimiteur T dans Notationsherbelin
2003-05-29Bug niveauherbelin
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
2003-05-27'only parsing' pour le passage de trucT a trucherbelin
2003-05-22V8Notationherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-04-29Blancsherbelin
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17Syntaxe 'x=y:>T'herbelin
2003-04-09Activation des implicites pour la v8herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
2003-03-31Notation eqT superflueherbelin
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2003-03-29Déplacement de minus dans Peanoherbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-21*** empty log message ***barras
2003-03-14*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
2002-12-15Une entrée spéciale "annot" pour les piquantsherbelin