aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* Prévention notations récursives sans terminal à gauche et qui font bouclerGravatar herbelin2007-03-15
* Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)Gravatar herbelin2007-02-24
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* Amélioration de l'automatisation des coupures quand deux idents se suiventGravatar herbelin2006-10-09
* Compatibilité hyp=var dans Tactic Notation + nettoyageGravatar herbelin2006-09-15
* Prise en compte de notations numérales définies au niveau utilisateur+ lég...Gravatar herbelin2006-01-08
* Réorganisation; suppression code mort; documentationGravatar herbelin2006-01-07
* Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...Gravatar herbelin2006-01-04
* Mini-restructurationGravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Correction printer des Tactic NotationGravatar herbelin2005-12-23
* Double bug de interp_modifiers anciennement caché par un troisième que les ...Gravatar herbelin2005-12-22
* Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...Gravatar herbelin2005-12-20
* Suppression de la mise en boite automatique si format utilisateurGravatar herbelin2005-12-19
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Correction bug Notation: il faut re-déclarer les règles de parsing des nota...Gravatar herbelin2004-11-22
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
* Non affichage des notations réduites à une variableGravatar herbelin2004-10-27
* Pas de notation v7 si purement en v8Gravatar herbelin2004-08-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* Correction bug #776Gravatar herbelin2004-06-28
* Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...Gravatar herbelin2004-03-27
* Amelioration affichage des notationsGravatar herbelin2004-03-17
* Mise en place de motifs récursifs dans Notation; quelques simplifications au...Gravatar herbelin2004-03-17
* Eviter la stricte redondance de regles de grammaires v7Gravatar herbelin2004-02-28
* Ajout de lconstr, constr et binder_constr dans Print Grammar constrGravatar herbelin2004-02-17
* Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R...Gravatar herbelin2004-02-13
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* Décomposition automatique des règles d'analyse syntaxique pour lesGravatar herbelin2004-02-12
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...Gravatar herbelin2004-01-29
* reparation de qqs bugs du traducteurGravatar barras2004-01-26
* Export information des references de notations pour coqdocGravatar herbelin2004-01-21
* Defaut d'information affichage en cas de notation incompatibleGravatar herbelin2004-01-05
* Suppression de l'espace avant les notations commencant par un identGravatar herbelin2003-12-19
* Traitement plus clair, notamment pour Locate, de quand quoter les composantes...Gravatar herbelin2003-11-22
* MAJ format et docGravatar herbelin2003-11-21
* Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarGravatar herbelin2003-11-15
* petits changements de syntaxeGravatar barras2003-11-12
* Fusion de tuple_constr/tuple_pattern dans operconstr/patternGravatar herbelin2003-11-08
* Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...Gravatar herbelin2003-11-01
* Ajout de Print VisibilityGravatar herbelin2003-10-28
* Bug des terminaux quotésGravatar herbelin2003-10-17
* En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...Gravatar herbelin2003-10-14