aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-07 20:50:30 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-07 21:00:02 +0100
commitdd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (patch)
tree2b61640b942b39650dec17ca077f28b5363aa843 /kernel/names.mli
parent89e59b9a578fa761ebc12e3a8e01c3b838301266 (diff)
Using Hashmaps by default in constant and inductive maps. This changes fold and
iter order, but it seems nobody was relying on it (contrarily to the string case).
Diffstat (limited to 'kernel/names.mli')
-rw-r--r--kernel/names.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index 4b71766bb..c85cfc433 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -319,8 +319,8 @@ end
(** The [*_env] modules consider an order on user part of names
the others consider an order on canonical part of names*)
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 Cset : CSig.SetS with type elt = Constant.t
+module Cset_env : CSig.SetS 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
@@ -386,7 +386,7 @@ sig
end
-module Mindset : Set.S with type elt = MutInd.t
+module Mindset : CSig.SetS 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