diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
-rw-r--r-- | plugins/firstorder/sequent.ml | 14 |
1 files changed, 8 insertions, 6 deletions
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) |