aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-04-10 16:04:02 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-04-10 16:04:02 +0200
commit22bda93212ec143402e7f2fb8dbff3b4485a0f9c (patch)
treec5a7e94c296a5a85de633146841a754753784ceb /kernel/names.ml
parent48e48837748764657303bd062801a7381a434d11 (diff)
Revert "refactoring: Names.DirPath.compare"
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml12
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index b91fa758f..da02a32a2 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