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 /kernel/indtypes.ml | |
| 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 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions