diff options
| author | Hugo Herbelin | 2020-07-14 15:57:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 17:38:36 +0100 |
| commit | 3ac39cdd88368c62aa25eaa37fb61fb16406e180 (patch) | |
| tree | 42bac084dab407796ed30816a2b70a6909f1eaf1 /doc/plugin_tutorial/tuto2 | |
| parent | 534d44074d0c4464b425ba9d7d92be8dda04d5ac (diff) | |
Moving the analysis of notation strings in notation.ml.
This is a better abstraction barrier (no "symbol" type with
uninterpreted ".." exported out of notation.ml). It also allows to
"browse" notations mentioning a "..".
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions