diff options
| author | Vincent Laporte | 2018-09-06 17:28:38 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-06 17:28:38 +0200 |
| commit | f6ed48098636f11362945d380bbe8cb71a9ab2ee (patch) | |
| tree | fdc69b612c5160aac16e8fdc09c5fb67991bd5af | |
| parent | 1877e1235c63ff3bbc958e5a79fa052ac852071c (diff) | |
Deprecation warning in legacy tacextend.mlp
| -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 |