From 72da3cc8c5cf607c9c461491760837de2161123e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 20 Jul 2018 18:01:18 +0200
Subject: Warnings on coercions used without being Imported

This warning makes it much easier to stop relying on `Set Automatic
Coercions Import`. Tested with success on math-classes.
---
 doc/sphinx/addendum/implicit-coercions.rst | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c0c4539564..23cbd76eda 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -325,6 +325,12 @@ Coercions and Modules
    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.
+
 Examples
 --------
 
-- 
cgit v1.2.3