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.
---
 CHANGES.md               |  3 +++
 plugins/ltac/g_class.mlg | 13 ++++++++++++-
 theories/Classes/Init.v  |  2 +-
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index af2b7991dd..59cc17c233 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -97,6 +97,9 @@ Tactics
 
 - Ltac backtraces can be turned on using the "Ltac Backtrace" option.
 
+- The syntax of the `autoapply` tactic was fixed to conform with preexisting
+  documentation: it now takes a `with` clause instead of a `using` clause.
+
 Vernacular commands
 
 - `Combined Scheme` can now work when inductive schemes are generated in sort
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
 
 {
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8a04206bb2..8732305953 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -23,7 +23,7 @@ Typeclasses Opaque id const flip compose arrow impl iff not all.
 
 (** Apply using the same opacity information as typeclass proof search. *)
 
-Ltac class_apply c := autoapply c using typeclass_instances.
+Ltac class_apply c := autoapply c with typeclass_instances.
 
 (** The unconvertible typeclass, to test that two objects of the same type are
    actually different. *)
-- 
cgit v1.2.3