aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_term.ml
Commit message (Expand)AuthorAge
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23