aboutsummaryrefslogtreecommitdiffhomepage
path: root/syntax
Commit message (Expand)AuthorAge
* Introduction d'un constructeur ARROW; rétablissement priorités desGravatar herbelin2002-11-20
* Correction des priorités des TOMATCHGravatar herbelin2002-11-20
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-28
* Bug qui empêchait "0" d'être parenthèséGravatar herbelin2002-10-21
* Parenthèses forcées autour des arguments d'une application pour parserGravatar herbelin2002-10-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* syntax/PPTactic.v passe au niveau MLGravatar herbelin2002-05-29
* Ajout EVALGravatar herbelin2002-05-29
* Ajout de Eval, Inst et CheckGravatar delahaye2002-05-27
* bad printing of Zeta reduction flags (was missing)Gravatar barras2002-02-11
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01
* Affichage NewInduction/NewDesctructGravatar herbelin2001-12-13
* Affichage des '_' pour IntrosGravatar herbelin2001-12-06
* Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bGravatar herbelin2001-11-08
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...Gravatar herbelin2001-10-05
* Mise en place d'un nouveau Destruct sur le modèle du nouvel InductionGravatar herbelin2001-08-05
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Reparation d'un bug d'affichage. Les let destructurants, if, et vieux CaseGravatar clrenard2001-06-11
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Reorganisation pour LtacGravatar delahaye2001-04-24
* Ajout de syntaxe pour LtacGravatar delahaye2001-04-23
* Reparation de l'affichage des THEN'sGravatar delahaye2001-04-13
* Bug affichage LETPATTERNGravatar herbelin2001-04-10
* Interprétation des qualidargGravatar herbelin2001-03-27
* Les règles d'affichage ajoutés dans le commit précédent avait le même no...Gravatar herbelin2001-03-23
* Règle de syntaxe pour CASTEDCOMMANDGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* Ajout du Match ContextGravatar delahaye2001-02-07
* Affichage des QUALIDGravatar herbelin2000-11-23
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...Gravatar herbelin2000-10-18
* Niveau d'associativité du letGravatar herbelin2000-10-11
* Code mort (2ème)Gravatar herbelin2000-10-05
* Code mortGravatar herbelin2000-10-05
* Renommage tactique Let en LetTacGravatar herbelin2000-10-03
* Bugs parenthèsesGravatar herbelin2000-09-14
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Réparation bug d'affichage et affichage des instanciations par des {...}Gravatar herbelin2000-05-23
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Affichage des <> pour débugGravatar herbelin2000-03-20
* BugsGravatar herbelin2000-01-11
* MAJGravatar herbelin2000-01-07
* Renommage command en constrGravatar herbelin2000-01-07
* Renommage command en constrGravatar herbelin2000-01-07
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* MAJGravatar herbelin1999-12-06
* PPMultipleCase.v -> PPCases.v et MAJGravatar herbelin1999-12-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 12:19:01 +0000