aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_zsyntax.ml
AgeCommit message (Expand)Author
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-04-16Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)letouzey
2007-11-07Replaced BinNat with a new version that is based on theories/Numbers/Natural/...emakarov
2006-02-04Branchement sur nouvelle interface de declare_numeral_interpreterherbelin
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrageherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-02-17Bug affichage entiers négatifsherbelin
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-11-10Correction bug #868herbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...herbelin
2003-11-05Interpretation des entiers dans N (ex-entier), maj du module des positiveherbelin
2003-09-12Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selonherbelin
2003-09-12MAJ module requis pour le parsing des numérauxherbelin
2003-03-12*** empty log message ***barras
2002-12-15Pas de 0 dans positiveherbelin
2002-11-25Z dans les patterns via les scopesherbelin
2002-11-24Installation des printers de nombres pour constr_exprherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-13compat ocaml 3.03filliatr
2001-08-10Parsingherbelin
2001-03-15entetesfilliatr
2000-10-18Mise en place de parseurs avec globalisation pas seulement dans les quotation...herbelin
1999-12-03compilation nativefilliatr