diff options
author | 2017-12-15 22:33:53 +0100 | |
---|---|---|
committer | 2017-12-18 17:17:06 +0100 | |
commit | 43c46c5398704e78c609f9ee3a51d515f2746f0e (patch) | |
tree | d1ab5c47b0c0985f8dd9e7406a2202483a1160ec /interp/discharge.mli | |
parent | b6e05e2944c2a7976c4ac1f51694b175f52dbaf8 (diff) |
[vernac] Cleanup of do_definition.
We remove a few old-style normalization and try to use the newer APIs,
however, it is hard to say whether the right magic is being used.
Diffstat (limited to 'interp/discharge.mli')
0 files changed, 0 insertions, 0 deletions