From 0a46af10ffc38726207bca952775102d48ad3b15 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 22 Sep 2020 18:36:10 +0200 Subject: Rename the GlobRef comparison modules following the standard pattern. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index d57c4f3abf..269e20c16e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -323,7 +323,7 @@ type key = | Oth let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 -- cgit v1.2.3