aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_term.ml
AgeCommit message (Expand)Author
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias