aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-10 02:37:41 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-11 10:59:23 +0200
commit2da7bf6327e1f35321f121de9560604b758f0472 (patch)
tree801a44dde07b604fcf5fa9d1e28270fe7319d4c6 /intf
parent4ebc7c27f04f2bcc3cf7160ae9ec177d1ca11707 (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 'intf')
-rw-r--r--intf/tacexpr.mli8
1 files changed, 1 insertions, 7 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index f821251c2..875ad3d16 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -377,19 +377,13 @@ type t_dispatch = <
constant:t_cst;
reference:t_ref;
name:t_nam;
- tacexpr:glob_tactic_expr;
+ tacexpr:unit;
level:tlevel
>
-type tactic_expr =
- t_dispatch gen_tactic_expr
-
type atomic_tactic_expr =
t_dispatch gen_atomic_tactic_expr
-type tactic_arg =
- t_dispatch gen_tactic_arg
-
(** Misc *)
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen