aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
2002-11-07Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' ↵herbelin
comme un entier de nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 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-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-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@3164 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-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-14La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsherbelin
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
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3125 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3124 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
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
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3122 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Bug de précédenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Hack pour parser '{x:T|P}*B' sans parenthesesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2728 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14petite erreur de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22Docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2492 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-19Uniformisation des theoremes dans Set et Type (def. de Acc_rect etbarras
well_founded_induction_type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2485 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14Syntaxe IF then else au lieu de either and_then or_elsebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-31changement generation de schema d'elimination, False_rec est primitif, ↵mohring
Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-29modification de la definition des def inductives unitaires et autorisation ↵mohring
d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-10Modifs incongrues dans le précédent commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2385 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-09MAJ des Id pour coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Suppression d'Export redondantsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2190 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27and_rec redondantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Deplacement des setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-30Fin de la modif Exc/optionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Correction d'un bug du pretty-printclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1770 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11documentation automatique de la bibliothèque standardfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Introduction d'une preuve de False_recmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Bug d'affichage à cause des << ... >>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1182 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Bug dans la règle de syntaxe de ex2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@867 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@816 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la ↵herbelin
déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris ↵herbelin
comme parseur par defaut; le type List devient AstList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@575 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 11:14:40 +0000