aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
Commit message (Expand)AuthorAge
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Affinement nommage des productionsGravatar herbelin2003-03-27
* *** empty log message ***Gravatar barras2003-03-12
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
* Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...Gravatar herbelin2002-12-04
* On force l'associativité pour les entrées sans niveauxGravatar herbelin2002-12-02
* Utilisation de Snext pour gérer les symboles non associatifsGravatar herbelin2002-11-29
* Ajout d'une entre Prim.bigintGravatar herbelin2002-11-28
* Affinement de la gestion des niveauxGravatar herbelin2002-11-28
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Compatibilité avec les << >> dans la très ancienne syntaxe des actionsGravatar herbelin2002-11-14
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
* Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageGravatar herbelin2002-10-13
* passage a ocaml 3.06Gravatar herbelin2002-09-27
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* Ajout de l'entrée ne_constrarg_listGravatar delahaye2002-03-19
* Meilleure gestion de la reduction dans FieldGravatar delahaye2002-03-17
* compat ocaml 3.03Gravatar filliatr2001-12-13
* TransparentGravatar barras2001-09-20
* ParsingGravatar herbelin2001-08-10
* Nouvelle entrée ident_or_numargGravatar herbelin2001-08-06
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la d...Gravatar herbelin2001-06-25
* Interpretation MetaId + Progress + InstGravatar delahaye2001-06-18
* Non parenthesage des applications de tactiquesGravatar delahaye2001-04-14
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* adding entry points for the arguments of the Comment command.Gravatar bertot2001-04-04
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* backtrack sur le lexeur de la V6Gravatar filliatr2001-01-30
* Réparation bug extensibilité de Constr.patternGravatar herbelin2001-01-19
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* ajout ident_or_constrarg pour NewInductionGravatar herbelin2000-12-20
* Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteGravatar herbelin2000-12-16
* Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le b...Gravatar herbelin2000-12-06
* Restruration autour de qualidargGravatar herbelin2000-11-26
* Ajout diverses entrées pour les noms qualifiésGravatar herbelin2000-11-20
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* 2èmeGravatar herbelin2000-10-18
* Mise en place de parseurs avec globalisation pas seulement dans les quotation...Gravatar herbelin2000-10-18
* Ajout castedopenconstrargGravatar herbelin2000-10-03
* Pattern matching de sous-termes + exceptions dans le lexerGravatar delahaye2000-08-17
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28