From 87b510e5b0f363724eae5db9f177f167a3586015 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 1 Mar 2014 18:26:26 +0100
Subject: Fixing pervasive comparisons

---
 plugins/firstorder/sequent.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'plugins/firstorder/sequent.ml')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 8b831d595..72bde18f4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -67,12 +67,14 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Globnames.RefOrdered.compare
-     =? (fun oc1 oc2 ->
-	   match oc1,oc2 with
-	       Some (m1,c1),Some (m2,c2) ->
-		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
-	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
+    let c = Globnames.RefOrdered.compare id1 id2 in
+    if c = 0 then
+      let cmp (i1, c1) (i2, c2) =
+        let c = Int.compare i1 i2 in
+        if c = 0 then OrderedConstr.compare c1 c2 else c
+      in
+      Option.compare cmp co1 co2
+    else c
 end
 
 module CM=Map.Make(OrderedConstr)
-- 
cgit v1.2.3