diff options
| author | Pierre-Marie Pédrot | 2014-05-16 16:21:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-16 16:23:12 +0200 |
| commit | 7491ffa371ab7537dd4d7b85af1079a792dd6e96 (patch) | |
| tree | 987805603bb5e3654dec49a9e1de209a66e5e093 /kernel | |
| parent | 842403acdbfe9812c45bd530cf6d9fa2a62842db (diff) | |
Tactics defined through TACTIC EXTEND that are only defined as a string do
not create grammar and printing rules anymore, they define Ltac entries
in the module that declares them instead.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions