aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.ml')
-rw-r--r--library/libnames.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index bb45369f2..e47ce86ca 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -195,8 +195,6 @@ module SpOrdered =
let compare = sp_ord
end
-module Spset = Set.Make(SpOrdered)
-module Sppred = Predicate.Make(SpOrdered)
module Spmap = Map.Make(SpOrdered)
let dirpath sp = let (p,_) = repr_path sp in p