diff options
| author | Emilio Jesus Gallego Arias | 2020-02-28 16:06:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-28 16:06:23 -0500 |
| commit | b095fc74b7f0be690a5313b992d4d4750c86875f (patch) | |
| tree | 8b4c5f5fb09e0ac6ba48ac2a9523259df83f9c33 /lib/pp.ml | |
| parent | 5c7d89641085e125471db089239e73a064073024 (diff) | |
[gramlib] Refactor gramlib interface.
This is in preparation for making the Gramlib interface the canonical
one; see #11647 .
I tried to implement some of the ideas that were floated around in a
chat with Pierre-Marie, suggestions / comments are welcome.
Diffstat (limited to 'lib/pp.ml')
0 files changed, 0 insertions, 0 deletions