From f3fb2f21646f257c0dd030a8411bafd80ea9d0bd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 13 Mar 2020 04:55:49 -0400
Subject: [cleanup] Remove unnecessary Map/Set module creation

---
 library/libnames.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'library/libnames.ml')

diff --git a/library/libnames.ml b/library/libnames.ml
index 126841c9a5..774212d0a3 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -78,9 +78,6 @@ let dirpath_of_string s =
   in
   DirPath.make path
 
-module Dirset = Set.Make(DirPath)
-module Dirmap = Map.Make(DirPath)
-
 (*s Section paths are absolute names *)
 
 type full_path = {
-- 
cgit v1.2.3