1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index b91fa758f9..da02a32a28 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -162,7 +162,17 @@ module DirPath =
 struct
   type t = module_ident list
 
-  let compare = List.compare Id.compare
+  let rec compare (p1 : t) (p2 : t) =
+    if p1 == p2 then 0
+    else begin match p1, p2 with
+    | [], [] -> 0
+    | [], _ -> -1
+    | _, [] -> 1
+    | id1 :: p1, id2 :: p2 ->
+      let c = Id.compare id1 id2 in
+      if Int.equal c 0 then compare p1 p2 else c
+    end
+
   let equal = List.equal Id.equal
 
   let rec hash accu = function