]> matita.cs.unibo.it Git - helm.git/commitdiff
- added module StringSet that implement set of string
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 15:49:17 +0000 (15:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 15:49:17 +0000 (15:49 +0000)
helm/http_getter/http_getter_types.ml

index 96977b6c546d51c51bb5b9d1207acb526f8b44c2..91c08c38b07604e1ca483e104265e8294334258a 100644 (file)
@@ -43,3 +43,5 @@ type http_getter_uri =
   | Xml_uri of http_getter_xml_uri
   | Rdf_uri of http_getter_rdf_uri
 
+module StringSet = Set.Make (String)
+