aboutsummaryrefslogtreecommitdiff
path: root/translate/pptacticnew.ml
AgeCommit message (Expand)Author
2003-06-10Raffinement diversherbelin
2003-05-24Ajout FreshIdherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-07coqide: toolbar/autosavemonate
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-27Reparation affichage LetTacherbelin
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Aérer les := et : de "assert"herbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-12*** empty log message ***barras
2003-02-05Ajout du traducteurdesmettr