diff options
| author | Gaëtan Gilbert | 2019-02-15 19:33:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-18 13:01:50 +0100 |
| commit | cfaf9d26c2a3d87641fba233098a0cae9f351d41 (patch) | |
| tree | 33679282da9587585f8344c6df588889642ded5a /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
Use named_context_val for fast lookup in intern named reference
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions