diff options
| author | Maxime Dénès | 2017-06-05 22:32:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-05 22:32:11 +0200 |
| commit | 5a5d37b83c487903963aa39799a1367752857da4 (patch) | |
| tree | ca0ef708964eae74cbc24fc30c570fcea22f991d /printing/miscprint.mli | |
| parent | 9a618ee0529f7153da1e10a8099a0b691bd13251 (diff) | |
| parent | a0ea7ebf4838903c3ed9a9b885716cf14134a0c8 (diff) | |
Merge PR#722: [printing] Remove duplicated printing function.
Diffstat (limited to 'printing/miscprint.mli')
| -rw-r--r-- | printing/miscprint.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/printing/miscprint.mli b/printing/miscprint.mli index fe8c779ff4..dbbe3dcfd8 100644 --- a/printing/miscprint.mli +++ b/printing/miscprint.mli @@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds val pr_move_location : ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds + +val pr_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_bindings_no_with : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_with_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds + |