diff options
Diffstat (limited to 'printing/richprinter.mli')
| -rw-r--r-- | printing/richprinter.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/printing/richprinter.mli b/printing/richprinter.mli index 261d22c4c3..c9e84e3eb4 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -34,6 +34,3 @@ val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp (** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) val richpp_constr : Constrexpr.constr_expr -> rich_pp - -(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *) -val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp |