diff options
| author | Pierre-Marie Pédrot | 2015-12-04 20:42:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-04 21:23:59 +0100 |
| commit | 0aba678e885fa53fa649de59eb1d06b4af3a847c (patch) | |
| tree | 127cd9e0e3600b17cf6b40e762e671ec9bf4628a /intf | |
| parent | 86304bddaff73bdc0f8aa6c7619d806c001040ec (diff) | |
Getting rid of the dynamic node of the tactic AST.
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 |