Added a more efficient way to recover the domain of a map.

The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 19 insertions, 7 deletions

diff --git a/library/assumptions.mli b/library/assumptions.mli
index f91412013c..cd08caf73c 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Environ
@@ -19,8 +20,9 @@ type context_object =
   | Transparent of constant (** A transparent constant *)
 
 (** AssumptionSet.t is a set of [assumption] *)
-module OrderedContextObject :  Set.OrderedType with type t = context_object
-module ContextObjectMap : Map.S with type key = context_object
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : Map.ExtS
+  with type key = context_object and module Set := ContextObjectSet
 
 (** collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type) *)
diff --git a/library/globnames.ml b/library/globnames.ml
index a04cdea8c8..e801970305 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Errors
 open Names
 open Term
diff --git a/library/globnames.mli b/library/globnames.mli
index 74da2cca89..4bf21cf0a1 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Names
 open Term
@@ -57,10 +58,12 @@ module RefOrdered_env : sig
 end
 
 module Refset : Set.S with type elt = global_reference
-module Refmap : Map.S with type key = global_reference
+module Refmap : Map.ExtS
+  with type key = global_reference and module Set := Refset
 
 module Refset_env : Set.S with type elt = global_reference
-module Refmap_env : Map.S with type key = global_reference
+module Refmap_env : Map.ExtS
+  with type key = global_reference and module Set := Refset_env
 
 (** {6 Extended global references } *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 80539a1565..4151e6774b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -192,8 +192,13 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-module OptionMap =
-  Map.Make (struct  type t = option_name let compare = compare end)
+module OptionOrd =
+struct
+  type t = option_name
+  let compare = compare
+end
+
+module OptionMap = Map.Make(OptionOrd)
 
 let value_tab = ref OptionMap.empty
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 627b8f013d..60ec7af790 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Loc
 open Names
@@ -37,7 +38,7 @@ val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t
 val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
 
 module Dirset : Set.S with type elt = DirPath.t
-module Dirmap : Map.S with type key = DirPath.t
+module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
 
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path