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