diff options
| author | Théo Zimmermann | 2019-12-02 08:35:38 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-02 08:58:28 +0100 |
| commit | a03543efc3ab66a846f392ea87897f7354c5a547 (patch) | |
| tree | 49d5c9aa41246b78a52fb5e48879874cac610ef2 | |
| parent | 20842fec926de9f5c05ade807ff86a22e6e88ba6 (diff) | |
Warn more clearly about incompatibilities coming from #10476.
| -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. |