diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 00:09:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 00:09:10 +0100 |
| commit | 3d5936f280bc01bd6baa8b4396e641ac156bfd5b (patch) | |
| tree | baa9bc67abdff13d159f4e4b05921bd2a89e7e49 /printing/printer.mli | |
| parent | d846451c9a07b4e051173878a5446edea029bf5b (diff) | |
Moving mutual inductive printing from Printer to Printmod.
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 |