aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Fixing #1960 (xml bug with external on goal variable) and #1961Gravatar herbelin2009-01-14
* - MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)Gravatar herbelin2008-10-26
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Correction de bugs:Gravatar herbelin2008-08-05
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 00:41:21 +0000