aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/table.mli')
-rw-r--r--plugins/extraction/table.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 916cf3ad6..4e638a0ac 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Miniml
open Declarations
module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : Map.S with type key = global_reference
+module Refmap' : CSig.MapS with type key = global_reference
val safe_basename_of_global : global_reference -> Id.t