diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f821251c27..875ad3d160 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 |