aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.mli
Commit message (Expand)AuthorAge
* *** empty log message ***Gravatar barras2003-12-23
* Globalisation des hints autorewriteGravatar herbelin2003-10-20
* Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...Gravatar herbelin2003-06-10
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* Re-ajout constrInGravatar herbelin2002-11-14
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29