aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-16 15:50:16 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-16 15:50:16 +0000
commit8bc0c8675a30eb54b6f9af5c19a6279de011c1ed (patch)
treeaabbec254b01295030188bb91fb386fc5a47cda3 /doc/stdlib
parent3876e19812d6476b732d0fd1a16d24058398794d (diff)
FSetPositive: sets of positive inspired by FMapPositive.
Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template4
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8f80d56ce..a4feb012b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -425,6 +425,7 @@ through the <tt>Require Import</tt> command.</p>
theories/MSets/MSetWeakList.v
theories/MSets/MSetList.v
theories/MSets/MSetAVL.v
+ theories/MSets/MSetPositive.v
theories/MSets/MSetToFiniteSet.v
(theories/MSets/MSets.v)
</dd>
@@ -444,8 +445,9 @@ through the <tt>Require Import</tt> command.</p>
theories/FSets/FSetList.v
theories/FSets/FSetWeakList.v
theories/FSets/FSetCompat.v
- (theories/FSets/FSets.v)
theories/FSets/FSetAVL.v
+ theories/FSets/FSetPositive.v
+ (theories/FSets/FSets.v)
theories/FSets/FSetToFiniteSet.v
theories/FSets/FMapInterface.v
theories/FSets/FMapWeakList.v