aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_rsyntax.ml
AgeCommit message (Expand)Author
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...herbelin
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
2003-02-27Interpretation des entiers dans les reels via les scopesdesmettr
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
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-07-19modifs de preuves (plus simples)mayero
2001-03-15entetesfilliatr
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
2000-12-22*** empty log message ***mayero
2000-11-23Ajout d'une syntaxe pour Reals.mayero