aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-06 17:19:58 +0200
committerMaxime Dénès2018-05-06 17:19:58 +0200
commitdad4731deed5c09e4e6cb212cd81462f7896c363 (patch)
tree413c52bbb7c67c228e20434ef2dfd6bd59c86753 /plugins/firstorder/instances.ml
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
parentafceace455a4b37ced7e29175ca3424996195f7b (diff)
Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e8c0b927dc..22a3e1f678 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -43,7 +43,7 @@ let compare_gr id1 id2 =
module OrderedInstance=
struct
- type t=instance * Globnames.global_reference
+ type t=instance * GlobRef.t
let compare (inst1,id1) (inst2,id2)=
(compare_instance =? compare_gr) inst2 inst1 id2 id1
(* we want a __decreasing__ total order *)