diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index ac35a324a..ad6cedf7d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -175,7 +175,3 @@ val set_printer_pr : printer_pr -> unit val default_printer_pr : printer_pr -(** Inductive declarations *) - -val pr_mutual_inductive_body : - env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds |