aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/vernacextend.ml4
Commit message (Expand)AuthorAge
* 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