diff options
| author | Emilio Jesus Gallego Arias | 2020-02-05 14:52:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:24:55 +0100 |
| commit | c3775de04c863c644ecfedffa23ddb17f99f2918 (patch) | |
| tree | ef25a343a4467c73dddd179c1b82567b902f05c7 /kernel/type_errors.mli | |
| parent | 9276876d66defa40adf0ff609c97150a6fe98d58 (diff) | |
[coqdep] Don't treat stdlib specially in boot mode.
This means the build system should pass the correct includes and
library bindings to `coqdep`.
We still have some discrepancies we won't be able to solve until
`Loadpath` and `coqdep` are fused [which depends on the dune build.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions