aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/sequent.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-22 18:36:10 +0200
committerPierre-Marie Pédrot2020-10-21 12:21:14 +0200
commit0a46af10ffc38726207bca952775102d48ad3b15 (patch)
tree03ca56bb87e50a5d33c29183f74058fc99302735 /plugins/firstorder/sequent.ml
parent0590764209dcb8540b5292aca38fe2df38b90ab9 (diff)
Rename the GlobRef comparison modules following the standard pattern.
Diffstat (limited to 'plugins/firstorder/sequent.ml')
-rw-r--r--plugins/firstorder/sequent.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index db3631daa4..99c5f85125 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
struct
type t = h_item
let compare (id1,co1) (id2,co2)=
- let c = GlobRef.Ordered.compare id1 id2 in
+ let c = GlobRef.CanOrd.compare id1 id2 in
if c = 0 then
let cmp (i1, c1) (i2, c2) =
let c = Int.compare i1 i2 in