diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pretty.ml | 2 | ||||
| -rw-r--r-- | parsing/pretty.mli | 5 |
2 files changed, 3 insertions, 4 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 641fa40356..00b598646c 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -6,7 +6,7 @@ open Util open Names open Generic open Term -open Constant +open Declarations open Inductive open Sign open Reduction diff --git a/parsing/pretty.mli b/parsing/pretty.mli index ae5ce0f252..e10c53b802 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 |