diff options
| author | Maxime Dénès | 2018-07-20 18:01:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-07 14:03:49 +0200 |
| commit | 72da3cc8c5cf607c9c461491760837de2161123e (patch) | |
| tree | 97c99dfc6b327b16ff15dd07c1bd8b940e6ed912 /doc | |
| parent | 51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff) | |
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.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 |
1 files changed, 6 insertions, 0 deletions
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 -------- |