aboutsummaryrefslogtreecommitdiff
path: root/syntax/PPTactic.v
AgeCommit message (Expand)Author
2002-05-29syntax/PPTactic.v passe au niveau MLherbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-02-11bad printing of Zeta reduction flags (was missing)barras
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
2001-12-13Affichage NewInduction/NewDesctructherbelin
2001-12-06Affichage des '_' pour Introsherbelin
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-04-24Reorganisation pour Ltacdelahaye
2001-04-23Ajout de syntaxe pour Ltacdelahaye
2001-04-13Reparation de l'affichage des THEN'sdelahaye
2001-04-10Bug affichage LETPATTERNherbelin
2001-03-27Interprétation des qualidargherbelin
2001-03-23Les règles d'affichage ajoutés dans le commit précédent avait le même no...herbelin
2001-03-22Règle de syntaxe pour CASTEDCOMMANDherbelin
2001-03-15entetesfilliatr
2001-02-07Ajout du Match Contextdelahaye
2000-11-21Traitement du pretty-print des Redexpdelahaye
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...herbelin
2000-10-03Renommage tactique Let en LetTacherbelin
2000-01-07Renommage command en constrherbelin
1999-12-06MAJherbelin
1999-12-05pretty-printfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:06:40 +0000