diff options
| author | Gaëtan Gilbert | 2019-07-02 13:59:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | bffe3e43a51420293960cc3c32845687bdee5f9b (patch) | |
| tree | 8928e9137f1652552d5c394c6d040aeb888812c5 /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | 48a377680f4f3b96f7c19c22f5641877c561f03d (diff) | |
Remove unused Decls.variable_{context,polymorphic}
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions