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.

1 files changed, 12 insertions, 1 deletions

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
 
 {