aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_basevernac.ml4
Commit message (Expand)AuthorAge
* 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
* Pb factorisation de Print GrammarGravatar herbelin2000-10-17
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...Gravatar herbelin2000-07-26
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Bête renommageGravatar herbelin2000-01-20
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
* Renommage command en constrGravatar herbelin2000-01-07
* compilation des grammaires (ouf)Gravatar filliatr1999-09-08
* modules grammaire CoqGravatar filliatr1999-09-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 13:29:53 +0000