From 150d190dfc60e462dfacafcfed3cabb58ff95365 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 15 Mar 2006 10:22:27 +0000
Subject: Ajout de theories/FSets contenant la partie "light" de FSets et FMap:
 pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs
 de proprietes.

Au passage, ajout de MoreList (complements de List) et SetoidList 
(quelques relations sur des listes considerees modulo un eq ou lt 
non standard.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FMap.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 theories/FSets/FMap.v

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

diff --git a/theories/FSets/FMap.v b/theories/FSets/FMap.v
new file mode 100644
index 0000000000..6950039685
--- /dev/null
+++ b/theories/FSets/FMap.v
@@ -0,0 +1,12 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id: FSet.v,v 1.2 2004/12/08 19:19:24 letouzey Exp $ *)
+
+Require Export FMapInterface.
+Require Export FMapList.
-- 
cgit v1.2.3