diff options
| author | Emilio Jesus Gallego Arias | 2020-10-15 13:00:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-10-21 20:16:34 +0200 |
| commit | f8a0b47dee445bb71e0824df576f69dd56511257 (patch) | |
| tree | d4e269c21882483c16b365ad90045798b06a3d14 /kernel/type_errors.ml | |
| parent | 9db73ef18c45238223f30a462fc2c6d20493d1d2 (diff) | |
[coqinit] Respect order of ML includes
This fixes a regression introduced in #11618, where I didn't realize
that the order of ML includes would be important as users may want to
shadow it.
In general I do believe that shadowing is tricky and the build system
should handle it, but for now makes sense to preserver the behavior.
The fix is not very nice, but we cannot afford to tweak the API as
this should be backported to 8.12.1; there is a pending PR refactoring
a bit more the toplevel init that should clean this up.
Fixes #12771
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions