From e5b5bbd6c6f084f4adf5859d98f46d2a6fa09910 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 May 2006 09:52:36 +0000
Subject: ajout d'exemples de decidable types

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8819 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/DecidableType.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'theories/FSets/DecidableType.v')

diff --git a/theories/FSets/DecidableType.v b/theories/FSets/DecidableType.v
index 4e34bbc0d1..a4de6ca7fe 100644
--- a/theories/FSets/DecidableType.v
+++ b/theories/FSets/DecidableType.v
@@ -31,6 +31,7 @@ Module Type DecidableType.
 
 End DecidableType. 
 
+(** * Additional notions about keys and datas used in FMap *)
 
 Module KeyDecidableType(D:DecidableType).
  Import D.
@@ -147,5 +148,9 @@ Module KeyDecidableType(D:DecidableType).
  Hint Unfold MapsTo In.
  Hint Resolve In_inv_2 In_inv_3.
 
-
 End KeyDecidableType.
+
+
+
+
+
-- 
cgit v1.2.3