diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/globnames.ml | 5 | ||||
| -rw-r--r-- | library/globnames.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 0ee82f0f7..02570d339 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -103,6 +103,11 @@ end module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) +(* Alternative sets and maps indexed by the user part of the kernel names *) + +module Refset_env = Set.Make(RefOrdered_env) +module Refmap_env = Map.Make(RefOrdered_env) + (* Extended global references *) type syndef_name = kernel_name diff --git a/library/globnames.mli b/library/globnames.mli index 1e6f143cd..1e53186f4 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -59,6 +59,9 @@ end module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +module Refset_env : Set.S with type elt = global_reference +module Refmap_env : Map.S with type key = global_reference + (** {6 Extended global references } *) type syndef_name = kernel_name |