diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 26cb1ca581..f221f0ed7d 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -24,8 +24,9 @@ The main changes brought by |Coq| version 8.11 are: - New `unsafe flags`__ to disable locally guard, positivity and universe checking. Reliance on these flags is always printed by :g:`Print Assumptions`. -- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have an impact - on user developments. +- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have a + significant impact on user developments (**common source of + incompatibility!**). - New interactive development method based on `vos` `interface files`__, allowing to work on a file without recompiling the proof parts of their dependencies. @@ -378,8 +379,14 @@ Changes in 8.11+beta1 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. + `Import A B`, the import of `B` was sometimes incomplete (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). + + .. warning:: + + This is a common source of incompatibilities in projects + migrating to Coq 8.11. + - **Changed:** Output generated by :flag:`Printing Dependent Evars Line` flag used by the Prooftree tool in Proof General. |