aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.mli
AgeCommit message (Expand)Author
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
2008-10-22Affichage des notations récursives:herbelin
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-03-31Ajout d'un choix 'onlyparse'herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin