aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-20 14:22:42 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-20 14:22:42 +0000
commitf03aaca003d9903bb90493a472a5f3138572a30e (patch)
treee4ca98b9e10b9ff0e9085b298b1cbe800f85d4c2
parentb78925e69d3e8b0ff2567bf0574e1bd55b33aa93 (diff)
Put Option in Clib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15631 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/lib.mllib1
2 files changed, 1 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 6ffbd25b1..d81113272 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,3 +8,4 @@ Xml_utils
Flags
CUnix
Envars
+Option \ No newline at end of file
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 93fb748ac..b99480bae 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -19,7 +19,6 @@ Explore
Predicate
Rtree
Heap
-Option
Dnet
Store
Unionfind