aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
| | | | | | | compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
| | | | | | | | compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) Déplacement de ~ au niveau 5 qui est le niveau des atomes propositionels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3175 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵Gravatar herbelin2002-10-22
| | | | | | l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une incompatibilité de nommage introduite lors du commit ↵Gravatar herbelin2002-10-22
| | | | | | précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3171 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3170 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
| | | | | | | variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en transparence des schémas d'induction bien-fondée sur SetGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3168 85f007b7-540e-0410-9357-904b9bb8a0f7
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Niveau d'affichage sumor/sumbool incohérent avec le parsingGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parenthèses manquantes pour se conformer à la doc (et au nouveau ↵Gravatar herbelin2002-10-21
| | | | | | PeanoSyntax.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug qui empêchait "0" d'être parenthèséGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure lisibilité grâce à tclTHENLISTGravatar herbelin2002-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation bug #180Gravatar herbelin2002-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'infixesGravatar herbelin2002-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsGravatar herbelin2002-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs dans la factorisation des règles de parsing de "{ ... } * ..."Gravatar herbelin2002-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moins de restriction sur le commit 1.5Gravatar herbelin2002-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsGravatar herbelin2002-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation du mécanisme des infixes quand ils commencent par une lettreGravatar herbelin2002-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parseur pour n>20 dans nat plus disponibleGravatar herbelin2002-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3152 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3150 85f007b7-540e-0410-9357-904b9bb8a0f7
* nom de fonction plus simpleGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3149 85f007b7-540e-0410-9357-904b9bb8a0f7
* pattern-matching avec cas inutilise dans closureGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3148 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit du calcul des dependances un peu plus robusteGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3146 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour NewtonIntGravatar desmettr2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrale de NewtonGravatar desmettr2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3144 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar desmettr2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3143 85f007b7-540e-0410-9357-904b9bb8a0f7
* TacCall attend une référenceGravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3142 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'application de ltac attend une référence; meilleure protection contreGravatar herbelin2002-10-14
| | | | | | | les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation bug Inversion (#212)Gravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pasGravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout optino_iterGravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parenthèses forcées autour des arguments d'une application pour parserGravatar herbelin2002-10-14
| | | | | | | les expressions comme "(f (x+1))" (anticipation sur nouvelle syntaxe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3135 85f007b7-540e-0410-9357-904b9bb8a0f7
* La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsGravatar herbelin2002-10-14
| | | | | | | de la forme "(1+...)" : remplacement par une approximation finie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneGravatar herbelin2002-10-14
| | | | | | | référence donnée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep bogué, retour sur version 1.75Gravatar herbelin2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3132 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage du chiffre 0Gravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3130 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵Gravatar herbelin2002-10-13
| | | | | | hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moins de restriction sur le commit précédentGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout map_rawconstrGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'ensembles de notations symboliques pour nat, Z et RGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3125 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
| | | | | | | Utilisation du parseur de constr pour les productions des règles de syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3122 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-05 00:02:50 +0000