diff options
Diffstat (limited to 'printing/richprinter.ml')
| -rw-r--r-- | printing/richprinter.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d95e19074..5f39f36ea 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -22,4 +22,3 @@ let make_richpp pr ast = let richpp_vernac = make_richpp RichppVernac.pr_vernac let richpp_constr = make_richpp RichppConstr.pr_constr_expr -let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env) |