Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspiwack-linear-comparison

Fixing a -1 -> +1 typo

1 files changed, 7 insertions, 8 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index cf0e371743..bec463ecf2 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
+  | 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
-  | 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
 
 let global_hash_gen hash_cst hash_ind hash_cons gr =
   let open Hashset.Combine in