diff options
| author | Johannes Kloos | 2017-10-24 01:07:18 +0200 |
|---|---|---|
| committer | Johannes Kloos | 2017-10-24 01:07:18 +0200 |
| commit | b57475e03b5d00b98829162ef6183b6c2655807c (patch) | |
| tree | 690b6b3eecedf4ece54c8d2568d20cc3dce52be7 /API/API.mli | |
| parent | e26b67436d12da63a11f0727c5b5895dfd03d249 (diff) | |
Fix #5413: [unfold ... in] not documented
Made a description of unfold...in and moved the index entry there.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions