aboutsummaryrefslogtreecommitdiff
path: root/parsing/vernacextend.ml4
AgeCommit message (Expand)Author
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