diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-01-13 17:38:27 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-01-13 17:38:27 +0100 |
| commit | 4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 (patch) | |
| tree | 5202a95f44355a5019680a6ae90a93fa169724d2 /theories/Structures/OrdersEx.v | |
| parent | 245affffb174fb26fc9a847abe44e01b107980a8 (diff) | |
MMaps: remove it from final 8.5 release, since this new library isn't mature enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
Diffstat (limited to 'theories/Structures/OrdersEx.v')
| -rw-r--r-- | theories/Structures/OrdersEx.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index b484257b9..89c563882 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -87,7 +87,7 @@ End PairOrderedType. (** Even if [positive] can be seen as an ordered type with respect to the usual order (see above), we can also use a lexicographic order over bits (lower bits are considered first). This is more natural when using - [positive] as indexes for sets or maps (see MSetPositive and MMapPositive. *) + [positive] as indexes for sets or maps (see MSetPositive). *) Local Open Scope positive. |