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

Fixing a -1 -> +1 typo

2 files changed, 18 insertions, 20 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index cf0e37174..bec463ecf 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
diff --git a/printing/printer.ml b/printing/printer.ml
index 70b5ffcc4..22bc122bd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -740,18 +740,17 @@ module OrderedContextObject =
 struct
   type t = context_object
   let compare x y =
-      match x , y with
-      | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
-      | Opaque k1 , Opaque k2 -> con_ord k1 k2
-      | Transparent k1 , Transparent k2 -> con_ord k1 k2
-      | Axiom _ , Variable _ -> 1
-      | Opaque _ , Variable _
-      | Opaque _ , Axiom _ -> 1
-      | Transparent _ , Variable _
-      | Transparent _ , Axiom _
-      | Transparent _ , Opaque _ -> 1
-      | _ , _ -> -1
+    match x , y with
+    | Variable i1 , Variable i2 -> Id.compare i1 i2
+    | Variable _ , _ -> -1
+    | _ , Variable _ -> 1
+    | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+    | Axiom _ , _ -> -1
+    | _ , Axiom _ -> 1
+    | Opaque k1 , Opaque k2 -> con_ord k1 k2
+    | Opaque _ , _ -> -1
+    | _ , Opaque _ -> 1
+    | Transparent k1 , Transparent k2 -> con_ord k1 k2
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)