From a03543efc3ab66a846f392ea87897f7354c5a547 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 2 Dec 2019 08:35:38 +0100 Subject: Warn more clearly about incompatibilities coming from #10476. --- doc/sphinx/changes.rst | 13 ++++++++++--- 1 file 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 `_, 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. -- cgit v1.2.3