aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorletouzey2006-03-15 10:22:27 +0000
committerletouzey2006-03-15 10:22:27 +0000
commit150d190dfc60e462dfacafcfed3cabb58ff95365 (patch)
treec650e4f52de0d687b412b4f251d85484e90372b0 /dev/include
parenta2cc7cc4e0aba3bd60129f4352926f5512cd8bf6 (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 'dev/include')
0 files changed, 0 insertions, 0 deletions