From 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 29 Oct 2015 20:52:32 +0100 Subject: Make the code of compare functions linear in the number of constructors. This scheme has been advised by @gashe on #79. Interestingly there are several comparison functions in Coq which were already implemented with this scheme. --- library/globnames.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'library/globnames.ml') diff --git a/library/globnames.ml b/library/globnames.ml index 3befaa9a9..5fdb6115e 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -112,12 +112,12 @@ let global_ord_gen ord_cst ord_ind ord_cons x y = | ConstructRef consx, ConstructRef consy -> ord_cons consx consy | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 - | ConstRef _, VarRef _ -> 1 - | ConstRef _, (IndRef _ | ConstructRef _) -> -1 - | IndRef _, (VarRef _ | ConstRef _) -> 1 - | IndRef _, ConstructRef _ -> -1 - | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 + | VarRef _, _ -> -1 + | _, VarRef _ -> 1 + | ConstRef _, _ -> -1 + | _, ConstRef _ -> 1 + | IndRef _, _ -> -1 + | _ , IndRef _ -> -1 let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in -- cgit v1.2.3