aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/SpecifSyntax.v
AgeCommit message (Collapse)Author
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵herbelin
TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Une entrée spéciale "annot" pour les piquantsherbelin
Positionnement du scope type_scope à certains endroits bien choisis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3445 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Simplificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Retablissement SynDef Value/Errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3278 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Généralisation de l'utilisation de Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3269 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3234 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-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-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-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-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-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-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-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 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
2000-04-30Bug affichage Error et Valueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@388 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Renommage command en constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-16erreurs de syntax :$filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@261 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13fichiers prelude Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@243 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 04:28:00 +0000