aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_basevernac.ml4
AgeCommit message (Expand)Author
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
2003-11-01Heritage des notations v7 seulement si zero information v8herbelin
2003-10-28Ajout de Print Visibilityherbelin
2003-10-23Independance de grammar.cmo vis a vis de Searchherbelin
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-26Ajout 'About'herbelin
2003-09-26Re-possibilite changement chaine infixe en passant v7 a v8herbelin
2003-09-22Distfix aussi adopte le nouveau schema de V8onlyherbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-19Mise en place des V8Notation et V8Infix pour déclarer des notations enherbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
2003-09-10Traduction de Distfixherbelin
2003-05-22Ajout V8Notationherbelin
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-08Ajout option "Local" à "Open Scope"herbelin
2003-03-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-01-06SearchAboutfilliatr
2002-12-15Meilleure factorisation des entrées NEXT internesherbelin
2002-11-29Raffinement syntaxe Infixherbelin
2002-11-28Oubliherbelin
2002-11-27Correction sur commit précédentherbelin
2002-11-25MAJ delimiters et niveaux d'associativiteherbelin
2002-11-25Retour sur le choix des delimiteursherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-07fix forbidden currified constructorsddr
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-07-15Pour assurer une compatibilite avec la 7.3herbelin
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
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-09-21Réparation des options Set Printing and coherbelin
2001-09-20Rajout 'Set Printing Depth'herbelin
2001-09-20Transparentbarras
2001-08-10Parsingherbelin
2001-05-29Facilites pour le debogguage des univers.coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 06:31:27 +0000