aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/lib.mllib
diff options
context:
space:
mode:
authorGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-26 11:08:34 +0000
committerGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-26 11:08:34 +0000
commit5dcc913519b8822ddf59eb3a356028f45f42cc3b (patch)
treea92cbe9fb3fdabff79163bb04e7d7f5bc87cbee7 /lib/lib.mllib
parent14893db7bda6542fa466508d962920ee64d3e45a (diff)
New functors for gmap and gset.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12417 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/lib.mllib')
-rw-r--r--lib/lib.mllib2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 56fe32cbd..d50adc776 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -12,6 +12,8 @@ Bstack
Edit
Gset
Gmap
+Fset
+Fmap
Tlm
tries
Gmapl