From d12cc91d07bc473276316474cc8f8beb9040934c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Jul 2018 18:22:24 +0200
Subject: Remove `Automatic Coercions Import` option.

This option made the Coercions command follow non-standard scoping rules
(effect on `Require` rather than `Import`). It was already marked for deletion
in 8.8.
---
 doc/sphinx/addendum/implicit-coercions.rst | 17 ++---------------
 1 file changed, 2 insertions(+), 15 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index d15aacad44..795fccbf08 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -322,21 +322,8 @@ are also forgotten.
 Coercions and Modules
 ---------------------
 
-.. flag:: Automatic Coercions Import
-
-   Since |Coq| version 8.3, the coercions present in a module are activated
-   only when the module is explicitly imported. Formerly, the coercions
-   were activated as soon as the module was required, whether it was
-   imported or not.
-
-   This option makes it possible to recover the behavior of the versions of
-   |Coq| prior to 8.3.
-
-.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
-
-   This warning is emitted when typechecking relies on a coercion
-   contained in a module that has not been explicitely imported. It helps
-   migrating code and stop relying on the option above.
+The coercions present in a module are activated only when the module is
+explicitly imported.
 
 Examples
 --------
-- 
cgit v1.2.3