aboutsummaryrefslogtreecommitdiff
path: root/intf/notation_term.ml
AgeCommit message (Expand)Author
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-07-26Adding support for recursive notations of the form "x , .. , y , z".Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-07Put all plugins behind an "API".Matej Kosik