diff options
Diffstat (limited to 'parsing/pretty.mli')
| -rw-r--r-- | parsing/pretty.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/pretty.mli b/parsing/pretty.mli index ae5ce0f25..e10c53b80 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -31,9 +31,8 @@ val print_val : env -> unsafe_judgment -> std_ppcmds val print_type : env -> unsafe_judgment -> std_ppcmds val print_eval : 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds -val implicit_args_msg : - section_path -> Constant.mutual_inductive_packet array -> std_ppcmds -val print_mutual : section_path -> Constant.mutual_inductive_body -> std_ppcmds +val print_mutual : + section_path -> Declarations.mutual_inductive_body -> std_ppcmds val print_name : identifier -> std_ppcmds val print_opaque_name : identifier -> std_ppcmds val print_local_context : unit -> std_ppcmds |