diff options
| author | letouzey | 2006-03-15 10:22:27 +0000 |
|---|---|---|
| committer | letouzey | 2006-03-15 10:22:27 +0000 |
| commit | 150d190dfc60e462dfacafcfed3cabb58ff95365 (patch) | |
| tree | c650e4f52de0d687b412b4f251d85484e90372b0 /theories/FSets/FMapWeak.v | |
| parent | a2cc7cc4e0aba3bd60129f4352926f5512cd8bf6 (diff) | |
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
Diffstat (limited to 'theories/FSets/FMapWeak.v')
| -rw-r--r-- | theories/FSets/FMapWeak.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/FSets/FMapWeak.v b/theories/FSets/FMapWeak.v new file mode 100644 index 0000000000..9e377d1d07 --- /dev/null +++ b/theories/FSets/FMapWeak.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 FMapWeakInterface. +Require Export FMapWeakList. |