diff options
Diffstat (limited to 'printing/printmod.mli')
| -rw-r--r-- | printing/printmod.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/printing/printmod.mli b/printing/printmod.mli index 8fd1cb4183..4c9245ee27 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> Pp.t -val print_module : bool -> ModPath.t -> Pp.t -val print_modtype : ModPath.t -> Pp.t + +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t +val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t |