blob: af38008a88c7161bdfcefa7bdfac0f8c1e3e945a (
plain)
1
2
3
4
5
6
|
- **Fixed:**
Two bugs in :cmd:`Export`. This can have an impact on the behavior of the
:cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports
`C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after
`Import A B`, the import of `B` was sometimes incomplete.
(`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès).
|
