diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 48ee955cc..b69a9955b 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -58,13 +58,3 @@ val pr_context_of : env -> std_ppcmds val emacs_str : string -> string -(*i*) -val fprterm_env : env -> constr -> std_ppcmds -val fprterm : constr -> std_ppcmds -val fprtype_env : env -> types -> std_ppcmds -val fprtype : types -> std_ppcmds - -(* For compatibility *) -val fterm0 : env -> constr -> std_ppcmds -(*i*) - |