diff options
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7b6010229..a0cffa596 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -11,6 +11,9 @@ open Libnames open Miniml open Declarations +module Refset' : Set.S with type elt = global_reference +module Refmap' : Map.S with type key = global_reference + val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) |