aboutsummaryrefslogtreecommitdiff
path: root/syntax
AgeCommit message (Expand)Author
2003-05-22Preservation affichage des ?n en V7herbelin
2003-05-19Affichage METAherbelin
2003-04-27Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-26Ajout de Set Print Widthgregoire
2003-01-16Bugs affichageherbelin
2002-11-20Introduction d'un constructeur ARROW; rétablissement priorités desherbelin
2002-11-20Correction des priorités des TOMATCHherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-21Bug qui empêchait "0" d'être parenthèséherbelin
2002-10-14Parenthèses forcées autour des arguments d'une application pour parserherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29syntax/PPTactic.v passe au niveau MLherbelin
2002-05-29Ajout EVALherbelin
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-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
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-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-05-29Facilites pour le debogguage des univers.coq
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-23Affichage des QUALIDherbelin
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-11Niveau d'associativité du letherbelin
2000-10-05Code mort (2ème)herbelin
2000-10-05Code mortherbelin
2000-10-03Renommage tactique Let en LetTacherbelin
2000-09-14Bugs parenthèsesherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-05-23Réparation bug d'affichage et affichage des instanciations par des {...}herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-03-20Affichage des <> pour débugherbelin
2000-01-11Bugsherbelin
2000-01-07MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:27:29 +0000