diff options
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |