diff options
| author | Pierre-Marie Pédrot | 2018-11-13 19:44:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-13 19:44:07 +0100 |
| commit | d384f58e5d910ec14574488f2744011cb09aa932 (patch) | |
| tree | 2b14c9d8bf601481ed96b84db31beb4689ce40ff /doc/plugin_tutorial/tuto1/src/simple_check.mli | |
| parent | 3e38d26233229d313d7a4c6015c7c15206c07305 (diff) | |
| parent | ccf995fd843f14ae8dfaf18177be6c2494faea35 (diff) | |
Merge PR #8760: Automatically generate names for universes.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.mli')
0 files changed, 0 insertions, 0 deletions