diff options
| author | Hugo Herbelin | 2017-11-07 15:24:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 18:03:56 +0100 |
| commit | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (patch) | |
| tree | f96740aedb3b99c54afd233e087a29b20a59cae3 /API/API.mli | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Was broken since 8.6.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions