diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 91d2531dd2..823b710cfe 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -12,7 +12,7 @@ open Globnames open Miniml open Declarations -module Refset' : Set.S with type elt = global_reference +module Refset' : CSig.SetS with type elt = global_reference module Refmap' : Map.S with type key = global_reference val safe_basename_of_global : global_reference -> Id.t |