diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e2995cfab..55d6e53a5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -185,8 +185,6 @@ and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg = | Reference of 'ref | TacCall of Loc.t * 'ref * ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list - | TacExternal of Loc.t * string * string * - ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr | TacPretype of 'trm |