aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate/pptacticnew.ml
Commit message (Expand)AuthorAge
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* petits changements de syntaxeGravatar barras2003-11-12
* Traduction semantique des InHyp de clause en InHypValue si local defGravatar herbelin2003-11-09
* 'as' avant 'using' dans 'destruct'Gravatar herbelin2003-11-09
* Added Instantiate ... inGravatar corbinea2003-11-06
* Divers bugs d'affichageGravatar herbelin2003-10-17
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* lettac -> setGravatar barras2003-10-16
* pr_tactic sans traduction; affichage InversionGravatar herbelin2003-10-10
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Ajout now_showGravatar herbelin2003-09-26
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* Système de renommage des noms de tactiques LtacGravatar herbelin2003-09-22
* Traduction de InstantiateGravatar herbelin2003-09-18
* Passage de lconstr à constr pour les arguments immédiat de commandesGravatar herbelin2003-09-06
* Bug et améliorations diversGravatar herbelin2003-08-31
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Formattage Apply withGravatar herbelin2003-06-23
* Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'Gravatar herbelin2003-06-19
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
* Raffinement diversGravatar herbelin2003-06-10
* Ajout FreshIdGravatar herbelin2003-05-24
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* coqide: toolbar/autosaveGravatar monate2003-05-07
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Localisation erreurs TacAlias; Globalisation moins tolérante dans lesGravatar herbelin2003-04-28
* Reparation affichage LetTacGravatar herbelin2003-04-27
* Localisation des appels de tactiques définies sans argumentsGravatar herbelin2003-04-14
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Aérer les := et : de "assert"Gravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* *** empty log message ***Gravatar barras2003-03-12
* Ajout du traducteurGravatar desmettr2003-02-05