aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/tacextend.ml4
Commit message (Expand)AuthorAge
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Affinements suite à extension Tactic Notation aux tacticiellesGravatar herbelin2005-05-17
* 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
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Protection contre les notations videsGravatar herbelin2003-11-26
* Simplification afficheur de tactiques non primitiveGravatar herbelin2003-09-18
* Adapter l'entree de grammaire a la version 7 ou 8Gravatar herbelin2003-09-06
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05
* Implante la macro camlp4 TACTIC EXTENDGravatar herbelin2002-05-29