diff options
| author | Pierre-Marie Pédrot | 2016-04-10 02:37:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-11 10:59:23 +0200 |
| commit | 2da7bf6327e1f35321f121de9560604b758f0472 (patch) | |
| tree | 801a44dde07b604fcf5fa9d1e28270fe7319d4c6 /printing/richprinter.mli | |
| parent | 4ebc7c27f04f2bcc3cf7160ae9ec177d1ca11707 (diff) | |
Removing the ad-hoc tactic_expr type.
This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.
Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.
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 |