aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_basevernac.ml4
AgeCommit message (Expand)Author
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-17Affinements suite à extension Tactic Notation aux tacticiellesherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-17Ajout 'Locate Module'herbelin
2004-07-16Nouvelle en-têteherbelin
2004-05-14Bug syntaxe AddPathherbelin
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...herbelin
2004-01-02meilleure presentation des commentaires du traducteurbarras
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 17:47:57 +0000