diff options
| author | Pierre-Marie Pédrot | 2020-11-09 18:22:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-12 13:59:22 +0100 |
| commit | c12471f1c5192ba1f18adac2109913c7b55ae50b (patch) | |
| tree | 7a65ae0926a49ff74a2c61c061d10dd52a1a235b /kernel/type_errors.ml | |
| parent | a0080f11d2d1702f5edb850a096b740fa2f905f7 (diff) | |
Statically ensure that the native interactive flag is always set to true.
It was a hidden invariant of the code.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions