diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 08:07:32 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-11 10:32:06 +0100 |
| commit | 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 (patch) | |
| tree | 770f78f58393646c20e0ba007f3bb10ea4784dde /printing/ppconstr.mli | |
| parent | 97f5f37f782ffb9914fa8f67e745ba1effad20be (diff) | |
[api] Move reduction modules to `tactics`
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index e7f71849a5..1cb3aa6d7a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t - -val pr_lident : lident -> Pp.t -val pr_lname : lname -> Pp.t - val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t val pr_sep_com : |