diff options
| author | Maxime Dénès | 2018-07-19 11:41:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 18:41:11 +0100 |
| commit | 264c208a5eb824c880ef4c46e060185470064df5 (patch) | |
| tree | ce99aabb06f6232d4ecfd2117269d827df24463c /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (diff) | |
Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions