diff options
| author | Gaëtan Gilbert | 2020-02-24 14:44:57 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | 2d6b7d5997037d9a94524a733867f64cd34e851c (patch) | |
| tree | 223fd7ad355643c956eaceb0c5eae45760b1de93 /library/globnames.mli | |
| parent | bbcf08fe1c0ab7e2cf21711f56230aaae93a1bdb (diff) | |
Add ExtRefMap/Set to globnames
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/globnames.mli b/library/globnames.mli index fb1583e16c..f5ed3a3ec7 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -61,3 +61,8 @@ module ExtRefOrdered : sig val equal : t -> t -> bool val hash : t -> int end + +module ExtRefSet : CSig.SetS with type elt = extended_global_reference +module ExtRefMap : CMap.ExtS + with type key = extended_global_reference + and module Set := ExtRefSet |