From 44d2955e49110a401d88c0449583b8c833887d9d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Mar 2020 12:27:29 +0100
Subject: Removing deprecated destruct syntax _eqn.

---
 doc/sphinx/language/gallina-specification-language.rst | 2 +-
 plugins/ltac/g_tactic.mlg                              | 8 --------
 2 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 12a9a30f3d..3b64465120 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -117,7 +117,7 @@ Other tokens
 
     ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn
+    <<: <= = => > >-> >= ? @ @{ [ [= ] _
     `( `{ { {| | |- || }
 
   When multiple tokens match the beginning of a sequence of characters,
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5a26ac8827..6a158bde17 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -185,10 +185,6 @@ let merge_occurrences loc cl = function
     in
     (Some p, ans)
 
-let warn_deprecated_eqn_syntax =
-  CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
-         (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
-
 (* Auxiliary grammar rules *)
 
 open Pvernac.Vernac_
@@ -461,10 +457,6 @@ GRAMMAR EXTEND Gram
   ;
   eqn_ipat:
     [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) }
-      | IDENT "_eqn"; ":"; pat = naming_intropattern ->
-         { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) }
-      | IDENT "_eqn" ->
-         { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) }
       | -> { None } ] ]
   ;
   as_name:
-- 
cgit v1.2.3


From 274ed99f9964b802e0a340c39ad69de4cabf37ff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Mar 2020 15:24:43 +0100
Subject: Change log

Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
---
 doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst

diff --git a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst
new file mode 100644
index 0000000000..827d484b28
--- /dev/null
+++ b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`.
+  Use `eqn:` syntax instead
+  (`#11877 <https://github.com/coq/coq/pull/11877>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3