diff options
| author | Pierre Letouzey | 2018-03-14 10:23:51 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:52 -0400 |
| commit | 64cb952f3fcf41c25a66a92bd124bba82e6db3f6 (patch) | |
| tree | 79e72103750c5be9e5c74e98c2a7ac3c25051b23 /interp/notation.mli | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Notation: no more chains of prim_token_interpreter
This cleanup prepares for forthcoming synchronization of prim_token_interpreter
wrt to Summary. These chains of prim_token_interpreter were anyway never used,
only one interpreter was declared per numeral scope.
After sync wrt Summary, we'll anyway be able to backtrack to a previous
interpreter.
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions