diff options
| author | Pierre-Marie Pédrot | 2018-09-07 13:44:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-07 13:44:44 +0200 |
| commit | 2139ee422754f4c3e039f7d3e3316fea47123b5c (patch) | |
| tree | c2f6c3c63ebb26f0f66ecbc2d4556048761ce5bf /grammar | |
| parent | 07c3905c30590c93f1b173833087bbd1df364227 (diff) | |
| parent | f6ed48098636f11362945d380bbe8cb71a9ab2ee (diff) | |
Merge PR #8423: coqpp: allow DEPRECATED when declaring tactics
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.mlp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 07239e7af0..5943600b7c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** WARNING: this file is deprecated; consider modifying coqpp instead. *) + (** Implementation of the TACTIC EXTEND macro. *) open Q_util |