From b08c14e551def3fb1ec885cf1ff05018f3d87ab9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 8 Feb 2019 13:47:47 +0100
Subject: Fix #7632: Change syntax of autoapply according to the documentation.

Deprecate the old syntax.
The documented syntax was using a with clause which is more standard with a hint database
than the using clause that was actually implemented.
---
 plugins/ltac/g_class.mlg | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 9ecc36bdf3..3f2fabeeee 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -99,8 +99,19 @@ TACTIC EXTEND is_ground
 | [ "is_ground" constr(ty) ] -> { is_ground ty }
 END
 
+{
+let deprecated_autoapply_using =
+  CWarnings.create
+    ~name:"autoapply-using" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.")
+}
+
 TACTIC EXTEND autoapply
-| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i }
+| [ "autoapply" constr(c) "using" preident(i) ] -> {
+    deprecated_autoapply_using ();
+    autoapply c i
+  }
+| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i }
 END
 
 {
-- 
cgit v1.2.3