diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-25 22:17:43 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-25 22:17:43 +0000 |
commit | 4d51d7e42125ecfec94768cac77e67026574c6f8 (patch) | |
tree | f0a375c9494f5ddb803c74bb97f6cbe1bd20cfc9 | |
parent | 9303e4590e52cba8c11fbacd91ff3098d7d1e00a (diff) |
Documentation of Set Automatic Coercions Import.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | doc/refman/Coercion.tex | 23 |
2 files changed, 25 insertions, 1 deletions
@@ -131,7 +131,8 @@ Module system - A functor application can be prefixed by a "!" to make it ignore any "Inline" annotation in the type of its argument(s) (for examples of use of the new features, see libraries Structures and Numbers). -- Coercions are now active only when modules are imported. +- Coercions are now active only when modules are imported (use "Set Automatic + Coercions Import" to get the behavior of the previous versions of Coq). Extraction diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 4f3d3ec41..3b6c949ba 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -367,6 +367,29 @@ Coercions with a local source class or a local target class, and coercions which do not verify the uniform inheritance condition any longer are also forgotten. +\asection{Coercions and Modules} +\index{Coercions!and modules} + +From 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, whatever it was +imported or not. + +To recover the behavior of the versions of Coq prior to 8.3, use the +following command: + +\comindex{Set Automatic Coercions Import} +\comindex{Unset Automatic Coercions Import} +\begin{verbatim} +Set Automatic Coercions Import. +\end{verbatim} + +To cancel the effect of the option, use instead: + +\begin{verbatim} +Unset Automatic Coercions Import. +\end{verbatim} + \asection{Examples} There are three situations: |