diff options
| author | Pierre-Marie Pédrot | 2014-05-20 18:25:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 19:40:23 +0200 |
| commit | b6fea49600a5b6089eeeea877f06f0e197a0eafb (patch) | |
| tree | 38ff75ba34bea37f0880cf6924ae0022d76e6875 /kernel | |
| parent | e705ae9d343c67212ce238899d21059ce93ee3e5 (diff) | |
Tactics declared through TACTIC EXTEND that are of the form
"foobar" constr(x1) ... constr(xn)
are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions