diff options
| author | Pierre-Marie Pédrot | 2016-04-11 11:02:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-11 11:02:27 +0200 |
| commit | 907db7ee1c9824aeedad7ce2d0f4f85225c36aba (patch) | |
| tree | 801a44dde07b604fcf5fa9d1e28270fe7319d4c6 /printing/richprinter.ml | |
| parent | c6a8c4b5fa590f2beecd73817497bd7773a87522 (diff) | |
| parent | 2da7bf6327e1f35321f121de9560604b758f0472 (diff) | |
Removing the typed-level tactic_expr type.
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 d95e190749..5f39f36eab 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) |