aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/vernacextend.ml4
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
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...Gravatar herbelin2007-08-24
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
* Hack peu élégant pour permettre de parser des listes avec séparateurs dans Gravatar herbelin2006-10-24
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
* Protection contre les notations videsGravatar herbelin2003-11-26
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* réparation de la protection contre les clauses indiscernables de TACTIC EXTE...Gravatar herbelin2002-10-12
* Implante la macro camlp4 VERNAC COMMAND EXTENDGravatar herbelin2002-05-29