aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate/pptacticnew.ml
Commit message (Expand)AuthorAge
* Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la...Gravatar herbelin2004-03-05
* Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...Gravatar herbelin2004-03-02
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Généralisation du type ltac Identifier en IntroPattern; prise en compte des...Gravatar herbelin2004-03-01
* Bugs/insuffisances trouvees en traduisant MModeGravatar herbelin2004-02-19
* reparation de qqs bugs du traducteurGravatar barras2004-01-26
* Corrige: Intros [] etait traduit intros (), qui ne reparse pasGravatar barras2004-01-16
* bugs avec Pose et AssertGravatar barras2004-01-09
* certains id n'etaient pas renommes pour eviter les conflits avec les mots-clesGravatar barras2004-01-05
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* *** empty log message ***Gravatar barras2003-12-24
* Reparation semantique casse de Pose en v7Gravatar herbelin2003-12-23
* *** empty log message ***Gravatar barras2003-12-23
* Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...Gravatar herbelin2003-12-22
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Symetrisation parsing/printing 'abstract'Gravatar herbelin2003-12-04
* Bug traduction clearbodyGravatar herbelin2003-12-01
* Renommage de tactiques ltac coincidant avec certaines tactiques primitivesGravatar herbelin2003-11-26
* Garder 'destruct using' a l'affichage ?Gravatar herbelin2003-11-25
* Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...Gravatar herbelin2003-11-25
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...Gravatar barras2003-11-13
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Mise en place systeme de renommage des noms de variables liees dans la biblio...Gravatar herbelin2003-11-12
* 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