aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.mli
AgeCommit message (Expand)Author
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