aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-10-22MAJherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-22Correction d'une incompatibilité de nommage introduite lors du commit précÃ...herbelin
2002-10-22majfilliatr
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21Mise en transparence des schémas d'induction bien-fondée sur Setherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-10-21Niveau d'affichage sumor/sumbool incohérent avec le parsingherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-21Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...herbelin
2002-10-21Bug qui empêchait "0" d'être parenthèséherbelin
2002-10-19Meilleure lisibilité grâce à tclTHENLISTherbelin
2002-10-19Réparation bug #180herbelin
2002-10-19Ajout d'infixesherbelin
2002-10-18Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsherbelin
2002-10-17Bugs dans la factorisation des règles de parsing de "{ ... } * ..."herbelin
2002-10-17Moins de restriction sur le commit 1.5herbelin
2002-10-17Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsherbelin
2002-10-16Réparation du mécanisme des infixes quand ils commencent par une lettreherbelin
2002-10-16Parseur pour n>20 dans nat plus disponibleherbelin
2002-10-16majfilliatr
2002-10-15nom de fonction plus simplebarras
2002-10-15pattern-matching avec cas inutilise dans closurebarras
2002-10-15commit du calcul des dependances un peu plus robustebarras
2002-10-15majfilliatr
2002-10-14MAJ pour NewtonIntdesmettr
2002-10-14Integrale de Newtondesmettr
2002-10-14*** empty log message ***desmettr
2002-10-14TacCall attend une référenceherbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-14Réparation bug Inversion (#212)herbelin
2002-10-14Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pasherbelin
2002-10-14Ajout optino_iterherbelin
2002-10-14Parenthèses forcées autour des arguments d'une application pour parserherbelin
2002-10-14La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-14coqdep bogué, retour sur version 1.75herbelin
2002-10-14majfilliatr
2002-10-13Bug affichage du chiffre 0herbelin
2002-10-13MAJherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-13Moins de restriction sur le commit précédentherbelin
2002-10-13Ajout map_rawconstrherbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-10-13Nettoyageherbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin