aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* Fix for notation scope & inductive typesGravatar vsiles2009-11-25
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove legacy export_* functionsGravatar glondu2009-09-29
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 03:25:31 +0000