diff options
Diffstat (limited to 'parsing/printmod.mli')
| -rw-r--r-- | parsing/printmod.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/printmod.mli b/parsing/printmod.mli index 2df0581c..a3a16e8e 100644 --- a/parsing/printmod.mli +++ b/parsing/printmod.mli @@ -14,4 +14,4 @@ val printable_body : dir_path -> bool val print_module : bool -> module_path -> std_ppcmds -val print_modtype : kernel_name -> std_ppcmds +val print_modtype : module_path -> std_ppcmds |