diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 9bf72b6600..438c338b8e 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -12,6 +12,16 @@ val gencompr : path_kind -> Coqast.t -> std_ppcmds val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds val gentacpr : Coqast.t -> std_ppcmds +val prterm : constr -> std_ppcmds +val prtype_env : 'a assumptions -> typed_type -> std_ppcmds +val prtype : typed_type -> std_ppcmds +val fprterm : constr -> std_ppcmds +val fprtype_env : 'a assumptions -> typed_type -> std_ppcmds +val fprtype : typed_type -> std_ppcmds +val fterm0 : 'a assumptions -> constr -> std_ppcmds +val term0 : 'a assumptions -> constr -> std_ppcmds +val term0_at_top : 'a assumptions -> constr -> std_ppcmds + val print_arguments : bool ref val print_casts : bool ref val print_emacs : bool ref |