aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-11-04ajout d'une entrée au makefile pour faire toutes les theories sauf les realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3205 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-04ajout d'un printer pour les global_referenceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3204 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-03Ajout delimiteurs dans les motifs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3203 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-03Moulinetteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3202 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-03Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3201 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3200 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-31L'extraction c'est magic cvs -n upletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3199 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3198 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-30Désagglutination du squelette de la notation et de sa précédenceherbelin
Premier jet pour Print Scope; Print Scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3197 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-30Optimisation du choix des niveaux intermédiaires dans une notation complexeherbelin
Désagglutination du squelette de la notation et de sa précédence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3196 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3195 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3191 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Mais laisser la syntaxe (!id) aussi disponible !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3190 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3189 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Parenthèse non obligatoires autour de !id sans argumentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3188 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Prise en compte let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3187 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3186 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3183 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-26code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3182 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque ↵herbelin
ces hypothèses étaient dépendantes dans d'autres hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3178 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Le test de redondance d'une règle était trop fortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3177 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
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
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
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
2002-10-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3174 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵herbelin
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
2002-10-22Correction d'une incompatibilité de nommage introduite lors du commit ↵herbelin
précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3171 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3170 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Mise en transparence des schémas d'induction bien-fondée sur Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3168 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Niveau d'affichage sumor/sumbool incohérent avec le parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3166 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3165 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Parenthèses manquantes pour se conformer à la doc (et au nouveau ↵herbelin
PeanoSyntax.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3163 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Bug qui empêchait "0" d'être parenthèséherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3162 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-19Meilleure lisibilité grâce à tclTHENLISTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3160 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-19Réparation bug #180herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3159 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-19Ajout d'infixesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3158 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-18Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3157 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-17Bugs dans la factorisation des règles de parsing de "{ ... } * ..."herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3156 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-17Moins de restriction sur le commit 1.5herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3155 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-17Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3154 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-16Réparation du mécanisme des infixes quand ils commencent par une lettreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3153 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-16Parseur pour n>20 dans nat plus disponibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3152 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3150 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15nom de fonction plus simplebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3149 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15pattern-matching avec cas inutilise dans closurebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3148 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-21 22:29:36 +0000