From f6ed48098636f11362945d380bbe8cb71a9ab2ee Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 6 Sep 2018 17:28:38 +0200
Subject: Deprecation warning in legacy tacextend.mlp

---
 grammar/tacextend.mlp | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
cgit v1.2.3