diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-07 20:50:30 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-07 21:00:02 +0100 |
commit | dd2a0175e3e35e5488c6f3b8a68c68845cbfcfd3 (patch) | |
tree | 2b61640b942b39650dec17ca077f28b5363aa843 /kernel/names.mli | |
parent | 89e59b9a578fa761ebc12e3a8e01c3b838301266 (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.mli | 6 |
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 |