diff options
Diffstat (limited to 'parsing/prettyp.mli')
| -rw-r--r-- | parsing/prettyp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index f8ea1ba1d..f106d16d6 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -35,7 +35,7 @@ val print_sec_context_typ : Nametab.qualid -> std_ppcmds val print_judgment : env -> unsafe_judgment -> std_ppcmds val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds val print_eval : - 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds + reduction_function -> env -> unsafe_judgment -> std_ppcmds (* This function is exported for the graphical user-interface pcoq *) val build_inductive : section_path -> int -> global_reference * rel_context * types * identifier array * types array |