aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppconstr.ml
AgeCommit message (Expand)Author
2003-11-18reparation bug moins unaire (erreur de PP)barras
2003-11-01Extensibilite de la grammaires des patternsherbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-12*** empty log message ***barras
2003-03-03Retour vieil afficheurherbelin
2003-02-27Retour nouvel afficheurherbelin
2003-01-19Rétablissement pr_patternherbelin
2003-01-07Retour printer ast pour V7.4herbelin
2002-12-21Affinement affichageherbelin
2002-12-15Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxeherbelin
2002-12-10Bugs diversherbelin
2002-12-09Problèmes et améliorations affichage; Changement Simplherbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-03bugs d'affichage (confusion key/scope dans les délimiteurs)herbelin
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_exprherbelin
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-09-27passage a ocaml 3.06herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin