diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 2 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 |