diff options
| author | Enrico | 2015-12-04 16:50:43 +0100 |
|---|---|---|
| committer | Enrico | 2015-12-04 16:50:43 +0100 |
| commit | 9adb94735e407167f312f218868df7576b631880 (patch) | |
| tree | cd6b4f5eb070f9f79f16392d191a8c4327d01752 | |
| parent | 672865bc8133d9cd60637f4cf696ed1388166d0a (diff) | |
Update ANNOUNCE-1.6.md
| -rw-r--r-- | etc/ANNOUNCE-1.6.md | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md index a5ad8cb..76c9356 100644 --- a/etc/ANNOUNCE-1.6.md +++ b/etc/ANNOUNCE-1.6.md @@ -40,8 +40,10 @@ The main incompatibility concerning users is the change of logical/physical path implied by the reorganization of the library. In particular "Require Ssreflect.ssreflect" does not work anymore. We propose a schema that is compatible with both Coq 8.4 and Coq 8.5, namely: - Require Import mathcomp.ssreflect.ssreflect. - From mathcomp Require Import ssrfun ssrbool ... + + Require Import mathcomp.ssreflect.ssreflect. + From mathcomp Require Import ssrfun ssrbool ... + The first line loads the ssreflect plugin using its full path. Then all other files are loaded from the mathcomp name space. The component part (like ssreflect or algebra) is omitted. All theory files in |