From 441ea07e3c8ba56b9e7d44e7802246dc06814415 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 30 Oct 2015 10:06:24 +0100 Subject: More uniformity in the style of comparison functions. --- library/globnames.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'library/globnames.ml') 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 -- cgit v1.2.3