aboutsummaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
AgeCommit message (Expand)Author
2004-08-23Pas de notation v7 si purement en v8herbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-28Correction bug #776herbelin
2004-03-27Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...herbelin
2004-03-17Amelioration affichage des notationsherbelin
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications au...herbelin
2004-02-28Eviter la stricte redondance de regles de grammaires v7herbelin
2004-02-17Ajout de lconstr, constr et binder_constr dans Print Grammar constrherbelin
2004-02-13Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R...herbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...herbelin
2004-01-26reparation de qqs bugs du traducteurbarras
2004-01-21Export information des references de notations pour coqdocherbelin
2004-01-05Defaut d'information affichage en cas de notation incompatibleherbelin
2003-12-19Suppression de l'espace avant les notations commencant par un identherbelin
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les composantes...herbelin
2003-11-21MAJ format et docherbelin
2003-11-15Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarherbelin
2003-11-12petits changements de syntaxebarras
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
2003-11-01Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...herbelin
2003-10-28Ajout de Print Visibilityherbelin
2003-10-17Bug des terminaux quotésherbelin
2003-10-14En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...herbelin
2003-10-14Changement 'as notation' en 'where notation'herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-09Nouveau format de l'option 'format'herbelin
2003-10-08Des abbreviations pour constrintern.mlherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-26Decouplage printing en v8 pour les interpretations de notationsherbelin
2003-09-25V8Infix declarait a tort une regle d'interpretation V7herbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-19parsingherbelin
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
2003-09-16Tentative amelioration pretty-printing symbolesherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
2003-09-10Traduction de Distfixherbelin
2003-08-11Nettoyageherbelin
2003-07-24Bug globalisation Grammar (suite)herbelin
2003-07-23Bug globalisationherbelin
2003-06-10Distinction mode v7 ou translate; conséquences du déplacement traducteur de...herbelin
2003-05-23Bug en mode translateherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Moins de ' ' à l'affichageherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:47:09 +0000