diff options
Diffstat (limited to 'plugins/extraction/common.mli')
| -rw-r--r-- | plugins/extraction/common.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 33c14e33a..b992f0557 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -43,7 +43,9 @@ 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 -> unit +(* In [push_visible], the [module_path list] corresponds to + module parameters, the innermost one coming first in the list *) +val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit val check_duplicate : module_path -> label -> string |