diff options
| author | Alasdair Armstrong | 2019-11-11 17:00:24 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-11-11 17:00:24 +0000 |
| commit | cd49c9df8e1d688327ae045729b538df00b77622 (patch) | |
| tree | c44354bb5ee44c165e9ac6e69795d1ae96c58a3f /src/interactive.mli | |
| parent | 20df613aee16ab0a1610bd9507c55d4fe48a43f3 (diff) | |
Make sure undefined_gen inserts enough type annotations for union constructors
Diffstat (limited to 'src/interactive.mli')
0 files changed, 0 insertions, 0 deletions