diff options
Diffstat (limited to 'printing/printmod.mli')
| -rw-r--r-- | printing/printmod.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/printmod.mli b/printing/printmod.mli index 7f7d34392..f3079d5b6 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -6,9 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Names (** false iff the module is an element of an open module type *) val printable_body : DirPath.t -> bool -include Printmodsig.Pp +val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds +val print_module : bool -> module_path -> std_ppcmds +val print_modtype : module_path -> std_ppcmds |