diff options
| author | Gaëtan Gilbert | 2018-10-02 16:13:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 456919dd31f2f4bda15c6b37e4f1217bc085fc41 (patch) | |
| tree | a21b255f9bb570b4df07885c894243e2481c000d /kernel/type_errors.ml | |
| parent | f3c1fe8bc7979cd7036fcd2a1b2fe8f0a1acb058 (diff) | |
Switch order eqappr/check relevance in conversion.
This takes advantage of the mutability of the fconstr relevance mark.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions