diff options
| author | Gaëtan Gilbert | 2019-10-28 16:48:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | 215b7e43cba768bfc82914718b159a22797f9d2b (patch) | |
| tree | 706f80870c1d18af5e920c518a3e7f09df3d6f69 /plugins/syntax/plugin_base.dune | |
| parent | ae1eb22a1365a6f477fc328eabf821fd346b5f0b (diff) | |
Move prettyp (Print implementation) to vernac/
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions