aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.ml
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-10-30 10:06:24 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-10-30 10:06:24 +0100
commit441ea07e3c8ba56b9e7d44e7802246dc06814415 (patch)
tree6f5b75969e49ab97e4ed1e03f8d09bed68306be5 /library/globnames.ml
parent48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 (diff)
More uniformity in the style of comparison functions.
Diffstat (limited to 'library/globnames.ml')
-rw-r--r--library/globnames.ml7
1 files changed, 3 insertions, 4 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 5fdb6115e..829e2cefc 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y =
let global_ord_gen ord_cst ord_ind ord_cons x y =
if x == y then 0
else match x, y with
- | ConstRef cx, ConstRef cy -> ord_cst cx cy
- | IndRef indx, IndRef indy -> ord_ind indx indy
- | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
| VarRef v1, VarRef v2 -> Id.compare v1 v2
-
| VarRef _, _ -> -1
| _, VarRef _ -> 1
+ | ConstRef cx, ConstRef cy -> ord_cst cx cy
| ConstRef _, _ -> -1
| _, ConstRef _ -> 1
+ | IndRef indx, IndRef indy -> ord_ind indx indy
| IndRef _, _ -> -1
| _ , IndRef _ -> -1
+ | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
let global_hash_gen hash_cst hash_ind hash_cons gr =
let open Hashset.Combine in