diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 96f282cac..a87f15deb 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -22,6 +22,8 @@ val fterm0 : 'a assumptions -> constr -> std_ppcmds val term0 : 'a assumptions -> constr -> std_ppcmds val term0_at_top : 'a assumptions -> constr -> std_ppcmds +val pr_ne_env : std_ppcmds -> path_kind -> context -> std_ppcmds + val prrawterm : Rawterm.rawconstr -> std_ppcmds val prpattern : Rawterm.pattern -> std_ppcmds |