diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index c401bd059..a68e72d26 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -45,7 +45,7 @@ val pp_global : kind -> global_reference -> string val pp_module : module_path -> string val top_visible_mp : unit -> module_path -val push_visible : module_path -> mod_self_id option -> unit +val push_visible : module_path -> module_path option -> unit val pop_visible : unit -> unit val check_duplicate : module_path -> label -> string |