diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
| commit | f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc (patch) | |
| tree | 95bf369c1f34a6a4c055357b68e60de58849bd11 /library/globnames.mli | |
| parent | 646c6765e5e3307f8898c4f63c405d91c2e6f47b (diff) | |
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
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/library/globnames.mli b/library/globnames.mli index 74da2cca8..4bf21cf0a 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 } *) |