diff options
author | Matej Košík <matej.kosik@inria.fr> | 2017-04-10 16:04:02 +0200 |
---|---|---|
committer | Matej Košík <matej.kosik@inria.fr> | 2017-04-10 16:04:02 +0200 |
commit | 22bda93212ec143402e7f2fb8dbff3b4485a0f9c (patch) | |
tree | c5a7e94c296a5a85de633146841a754753784ceb /kernel/names.ml | |
parent | 48e48837748764657303bd062801a7381a434d11 (diff) |
Revert "refactoring: Names.DirPath.compare"
This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16.
Diffstat (limited to 'kernel/names.ml')
-rw-r--r-- | kernel/names.ml | 12 |
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 |