aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-28majfilliatr
2002-10-26code mortherbelin
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...herbelin
2002-10-23Le test de redondance d'une règle était trop fortherbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 07:18:10 +0000