aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_basevernac.ml4
Commit message (Expand)AuthorAge
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* *** empty log message ***Gravatar barras2003-03-21
* *** empty log message ***Gravatar barras2003-03-12
* SearchAboutGravatar filliatr2003-01-06
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
* Raffinement syntaxe InfixGravatar herbelin2002-11-29
* OubliGravatar herbelin2002-11-28
* Correction sur commit précédentGravatar herbelin2002-11-27
* MAJ delimiters et niveaux d'associativiteGravatar herbelin2002-11-25
* Retour sur le choix des delimiteursGravatar herbelin2002-11-25
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* fix forbidden currified constructorsGravatar ddr2002-11-07
* Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...Gravatar herbelin2002-10-22
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
* Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneGravatar herbelin2002-10-14
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...Gravatar herbelin2002-10-13
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Pour assurer une compatibilite avec la 7.3Gravatar herbelin2002-07-15
* 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
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Réparation des options Set Printing and coGravatar herbelin2001-09-21
* Rajout 'Set Printing Depth'Gravatar herbelin2001-09-20
* TransparentGravatar barras2001-09-20
* ParsingGravatar herbelin2001-08-10
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* nettoyage d'entrees de grammaires inutilesGravatar courant2001-04-09
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* bug Print Proof; usage coqtop/coqcGravatar filliatr2001-04-06
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* Adding A command for comments, this makes it possible to have structuredGravatar bertot2001-04-04
* entetesGravatar filliatr2001-03-15
* Ajout d'une commande pour afficher chaque coercion à la demandeGravatar herbelin2001-02-06
* Correction pour Time pour ne pas etre oblige de mettre deux pointsGravatar delahaye2001-02-05
* Ajout option Set/Unset/Test Printing CoercionsGravatar herbelin2001-01-31
* Factorisation du '.' finalGravatar herbelin2001-01-27
* Token n'est plus un keywordGravatar herbelin2000-12-25
* Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteGravatar herbelin2000-12-16
* Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...Gravatar herbelin2000-12-15
* Now AddRecPath and AddPath can be used with an As option to specify theGravatar sacerdot2000-11-29
* Restruration autour de qualidargGravatar herbelin2000-11-26
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ...Gravatar herbelin2000-11-20
* nouveau load pathGravatar filliatr2000-11-08
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...Gravatar herbelin2000-10-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 01:44:55 +0000