aboutsummaryrefslogtreecommitdiff
path: root/parsing/vernacextend.ml4
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
2006-10-24Hack peu élégant pour permettre de parser des listes avec séparateurs dans herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Abstraction vis a vis de dummy_locherbelin
2003-11-26Protection contre les notations videsherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-12réparation de la protection contre les clauses indiscernables de TACTIC EXTE...herbelin
2002-05-29Implante la macro camlp4 VERNAC COMMAND EXTENDherbelin