diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 22 | ||||
| -rw-r--r-- | kernel/names.mli | 30 |
2 files changed, 21 insertions, 31 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 9124b46897..2a04ff3c55 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -58,15 +58,7 @@ struct end module Set = Set.Make(Self) - module Map = - struct - include Map.Make(Self) - exception Finded - let exists f m = - try iter (fun a b -> if f a b then raise Finded) m ; false - with Finded -> true - let singleton k v = add k v empty - end + module Map = CMap.Make(Self) module Pred = Predicate.Make(Self) @@ -218,7 +210,7 @@ struct end -module MBImap = Map.Make(MBId) +module MBImap = CMap.Make(MBId) module MBIset = Set.Make(MBId) (** {6 Names of structure elements } *) @@ -298,7 +290,7 @@ module ModPath = struct end module MPset = Set.Make(ModPath) -module MPmap = Map.Make(ModPath) +module MPmap = CMap.Make(ModPath) (** {6 Kernel names } *) @@ -357,7 +349,7 @@ module KerName = struct end -module KNmap = Map.Make(KerName) +module KNmap = CMap.Make(KerName) module KNpred = Predicate.Make(KerName) module KNset = Set.Make(KerName) @@ -467,8 +459,8 @@ end module Constant = KerPair -module Cmap = Map.Make(Constant.CanOrd) -module Cmap_env = Map.Make(Constant.UserOrd) +module Cmap = CMap.Make(Constant.CanOrd) +module Cmap_env = CMap.Make(Constant.UserOrd) module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Set.Make(Constant.CanOrd) module Cset_env = Set.Make(Constant.UserOrd) @@ -477,7 +469,7 @@ module Cset_env = Set.Make(Constant.UserOrd) module MutInd = KerPair -module Mindmap = Map.Make(MutInd.CanOrd) +module Mindmap = CMap.Make(MutInd.CanOrd) module Mindset = Set.Make(MutInd.CanOrd) module Mindmap_env = Map.Make(MutInd.UserOrd) diff --git a/kernel/names.mli b/kernel/names.mli index c05e30b9b5..82df075626 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util + (** {6 Identifiers } *) module Id : @@ -35,7 +37,7 @@ sig module Set : Set.S with type elt = t (** Finite sets of identifiers. *) - module Map : Map.S with type key = t + module Map : Map.ExtS with type key = t and module Set := Set (** Finite maps of identifiers. *) module Pred : Predicate.S with type elt = t @@ -133,7 +135,7 @@ sig (** Pretty-printer. *) module Set : Set.S with type elt = t - module Map : Map.S with type key = t + module Map : Map.ExtS with type key = t and module Set := Set end @@ -170,7 +172,7 @@ sig end module MBIset : Set.S with type elt = MBId.t -module MBImap : Map.S with type key = MBId.t +module MBImap : Map.ExtS with type key = MBId.t and module Set := MBIset (** {6 The module part of the kernel name } *) @@ -194,7 +196,7 @@ sig end module MPset : Set.S with type elt = ModPath.t -module MPmap : Map.S with type key = ModPath.t +module MPmap : Map.ExtS with type key = ModPath.t and module Set := MPset (** {6 The absolute names of objects seen by kernel } *) @@ -222,7 +224,7 @@ end module KNset : Set.S with type elt = KerName.t module KNpred : Predicate.S with type elt = KerName.t -module KNmap : Map.S with type key = KerName.t +module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset (** {6 Constant Names } *) @@ -288,11 +290,11 @@ end (** The [*_env] modules consider an order on user part of names the others consider an order on canonical part of names*) -module Cmap : Map.S with type key = Constant.t -module Cmap_env : Map.S with type key = Constant.t -module Cpred : Predicate.S with type elt = Constant.t -module Cset : Set.S with type elt = Constant.t +module Cpred : Predicate.S with type elt = Constant.t +module Cset : Set.S with type elt = Constant.t module Cset_env : Set.S with type elt = Constant.t +module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset +module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env (** {6 Inductive names} *) @@ -352,9 +354,9 @@ sig end -module Mindmap : Map.S with type key = MutInd.t -module Mindmap_env : Map.S with type key = MutInd.t module Mindset : Set.S with type elt = MutInd.t +module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset +module Mindmap_env : Map.S with type key = MutInd.t (** Beware: first inductive has index 0 *) type inductive = MutInd.t * int @@ -448,11 +450,7 @@ module Idset : Set.S with type elt = identifier and type t = Id.Set.t module Idpred : Predicate.S with type elt = identifier and type t = Id.Pred.t (** @deprecated Same as [Id.Pred]. *) -module Idmap : sig - include Map.S with type key = identifier - val exists : (identifier -> 'a -> bool) -> 'a t -> bool - val singleton : key -> 'a -> 'a t -end +module Idmap : module type of Id.Map (** @deprecated Same as [Id.Map]. *) (** {5 Directory paths} *) |