diff options
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 | ||||
| -rw-r--r-- | kernel/names.ml | 8 | ||||
| -rw-r--r-- | kernel/names.mli | 4 | ||||
| -rw-r--r-- | library/coqlib.ml | 2 | ||||
| -rw-r--r-- | library/globnames.ml | 6 | ||||
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | pretyping/keys.ml | 6 | ||||
| -rw-r--r-- | printing/printer.ml | 2 | ||||
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
12 files changed, 20 insertions, 20 deletions
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 diff --git a/interp/reserve.ml b/interp/reserve.ml index 4418a32645..1d5af3ff39 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -28,7 +28,7 @@ type key = (** TODO: share code from Notation *) 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 diff --git a/kernel/names.ml b/kernel/names.ml index 5f2ecea5f0..f7658df355 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -991,7 +991,7 @@ module GlobRef = struct (* By default, [global_reference] are ordered on their canonical part *) - module Ordered = struct + module CanOrd = struct open Constant.CanOrd type t = GlobRefInternal.t let compare gr1 gr2 = @@ -1000,7 +1000,7 @@ module GlobRef = struct let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr end - module Ordered_env = struct + module UserOrd = struct open Constant.UserOrd type t = GlobRefInternal.t let compare gr1 gr2 = @@ -1010,12 +1010,12 @@ module GlobRef = struct let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr end - module Map = HMap.Make(Ordered) + module Map = HMap.Make(CanOrd) module Set = Map.Set (* Alternative sets and maps indexed by the user part of the kernel names *) - module Map_env = HMap.Make(Ordered_env) + module Map_env = HMap.Make(UserOrd) module Set_env = Map_env.Set end diff --git a/kernel/names.mli b/kernel/names.mli index a0320fda43..76be6ca105 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -667,14 +667,14 @@ module GlobRef : sig val equal : t -> t -> bool - module Ordered : sig + module CanOrd : sig type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end - module Ordered_env : sig + module UserOrd : sig type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool 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 diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index f13901c36d..4adad53899 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -38,7 +38,7 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else GlobRef.Ordered.compare id1 id2 + else GlobRef.CanOrd.compare id1 id2 module OrderedInstance= struct 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 diff --git a/pretyping/keys.ml b/pretyping/keys.ml index 7a7099c195..dd3488c1df 100644 --- a/pretyping/keys.ml +++ b/pretyping/keys.ml @@ -34,7 +34,7 @@ module KeyOrdered = struct let hash gr = match gr with - | KGlob gr -> 9 + GlobRef.Ordered.hash gr + | KGlob gr -> 9 + GlobRef.CanOrd.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 @@ -49,14 +49,14 @@ module KeyOrdered = struct let compare gr1 gr2 = match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 + | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.compare gr1 gr2 | _, KGlob _ -> -1 | KGlob _, _ -> 1 | k, k' -> Int.compare (hash k) (hash k') let equal k1 k2 = match k1, k2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 + | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.equal gr1 gr2 | _, KGlob _ -> false | KGlob _, _ -> false | k, k' -> k == k' diff --git a/printing/printer.ml b/printing/printer.ml index bc26caefbe..be1cc0d64a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -884,7 +884,7 @@ struct MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 | TypeInType k1, TypeInType k2 -> - GlobRef.Ordered.compare k1 k2 + GlobRef.CanOrd.compare k1 k2 | Constant _, _ -> -1 | _, Constant _ -> 1 | Positive _, _ -> -1 diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index f721e9956b..af0ca22868 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -27,7 +27,7 @@ type term_label = | SortLabel let compare_term_label t1 t2 = match t1, t2 with -| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2 +| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2 | _ -> pervasives_compare t1 t2 (** OK *) type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 3bcd235b41..fee9dd1b96 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -107,7 +107,7 @@ struct | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 | DSort, _ -> -1 | _, DSort -> 1 - | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2 + | DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2 | DRef _, _ -> -1 | _, DRef _ -> 1 | DCtx (tl1, tr1), DCtx (tl2, tr2) |