diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 73130d3804..ead221c5fb 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -209,7 +209,6 @@ constraint 'a = < (** Possible arguments of a tactic definition *) and 'a gen_tactic_arg = - | TacDynamic of Loc.t * Dyn.t | TacGeneric of 'lev generic_argument | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval |