diff options
| author | Pierre-Marie Pédrot | 2019-10-03 14:44:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-03 14:44:41 +0200 |
| commit | 3612ac1f639e361504cf3b2ded5609f5b643dfaa (patch) | |
| tree | f96700b564efb9d7c55d95dc0aebbe5561882b51 /printing/printmod.mli | |
| parent | 92a55bf800a34b5ec283ce0419cde98f3312c9b8 (diff) | |
| parent | cca4665778dd799e5802594761e13b8d53502824 (diff) | |
Merge PR #10727: [library] Move `Declaremods` to `vernac/`
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
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 |