diff options
| author | Pierre-Marie Pédrot | 2020-09-22 18:36:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:21:14 +0200 |
| commit | 0a46af10ffc38726207bca952775102d48ad3b15 (patch) | |
| tree | 03ca56bb87e50a5d33c29183f74058fc99302735 /library | |
| parent | 0590764209dcb8540b5292aca38fe2df38b90ab9 (diff) | |
Rename the GlobRef comparison modules following the standard pattern.
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 2 | ||||
| -rw-r--r-- | library/globnames.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 04a6e159eb..b374ecbca0 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -84,7 +84,7 @@ let gen_reference_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in let all = Nametab.locate_all qualid in - let all = List.sort_uniquize GlobRef.Ordered_env.compare all in + let all = List.sort_uniquize GlobRef.UserOrd.compare all in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> x diff --git a/library/globnames.ml b/library/globnames.ml index bc24fbf096..654349dea0 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -98,14 +98,14 @@ module ExtRefOrdered = struct let equal x y = x == y || match x, y with - | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.equal rx ry | SynDef knx, SynDef kny -> KerName.equal knx kny | (TrueGlobal _ | SynDef _), _ -> false let compare x y = if x == y then 0 else match x, y with - | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.compare rx ry | SynDef knx, SynDef kny -> KerName.compare knx kny | TrueGlobal _, SynDef _ -> -1 | SynDef _, TrueGlobal _ -> 1 @@ -113,7 +113,7 @@ module ExtRefOrdered = struct open Hashset.Combine let hash = function - | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr) + | TrueGlobal gr -> combinesmall 1 (GlobRef.UserOrd.hash gr) | SynDef kn -> combinesmall 2 (KerName.hash kn) end |