diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 14:43:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 18:53:09 +0200 |
| commit | 7045848145c16d978456aab2edd192c54d242e69 (patch) | |
| tree | 2d4e3f69a6ef6fe22cd0373c84ebf551c98af849 /printing/genprint.mli | |
| parent | 52c3917be7239f7d5ab1ba882275b4571463f585 (diff) | |
Unplugging Pptactic from Ppvernac.
Diffstat (limited to 'printing/genprint.mli')
| -rw-r--r-- | printing/genprint.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/printing/genprint.mli b/printing/genprint.mli index 6e6626f2f..5381fc5bd 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -11,6 +11,8 @@ open Pp open Genarg +type 'a printer = 'a -> std_ppcmds + val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds (** Printer for raw level generic arguments. *) @@ -20,9 +22,9 @@ val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds (** Printer for top level generic arguments. *) -val generic_raw_print : rlevel generic_argument -> std_ppcmds -val generic_glb_print : glevel generic_argument -> std_ppcmds -val generic_top_print : tlevel generic_argument -> std_ppcmds +val generic_raw_print : rlevel generic_argument printer +val generic_glb_print : glevel generic_argument printer +val generic_top_print : tlevel generic_argument printer val register_print0 : ('raw, 'glb, 'top) genarg_type -> - ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit + 'raw printer -> 'glb printer -> 'top printer -> unit |