aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/vernacextend.ml4
Commit message (Expand)AuthorAge
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* Fix compilation with camlp5 (Closes: #2487)Gravatar glondu2011-01-25
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - 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