aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.ml
AgeCommit message (Expand)Author
2006-01-03Redéclaration de la notation à l'import pour être cohérent avec l'activat...herbelin
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...herbelin
2005-01-03HUGE COMMITsacerdot
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-01Renommage Topconstr.map_aconstr_with_binders_locherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-03-31Ajout d'un choix 'onlyparse'herbelin
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin