From 7f67c70bec6a13ed0e39548e4439f962ac5dcd79 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 26 Jul 2019 13:55:00 +0200
Subject: Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`

Fixes #10576
---
 tools/coqdoc/output.ml |  2 +-
 vernac/g_vernac.mlg    | 10 +---------
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 717c06a868..ae1e1c6ed3 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -30,7 +30,7 @@ let build_table l =
 
 let is_keyword =
   build_table
-    [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
+    [ "About"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
       "Export"; "Fact"; "Fix"; "Fixpoint"; "From"; "Function"; "Generalizable"; "Global"; "Grammar";
       "Guarded"; "Goal"; "Hint"; "Debug"; "On";
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3095ab3fe1..8d6724c3b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -939,15 +939,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
           { VernacRemoveLoadPath dir }
 
-       (* For compatibility *)
-      | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath ->
-          { VernacAddLoadPath (false, dir, alias) }
-      | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath ->
-          { VernacAddLoadPath (true, dir, alias) }
-      | IDENT "DelPath"; dir = ne_string ->
-          { VernacRemoveLoadPath dir }
-
-      (* Type-Checking (pas dans le refman) *)
+      (* Type-Checking *)
       | "Type"; c = lconstr -> { VernacGlobalCheck c }
 
       (* Printing (careful factorization of entries) *)
-- 
cgit v1.2.3


From 2f33fce7ac580d1966476d6d2c0f06a3ec920e6d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 27 Nov 2019 20:24:31 +0100
Subject: Changelog entry for #11187.

---
 doc/changelog/07-commands-and-options/11187-remove-addpath.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/11187-remove-addpath.rst

diff --git a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst
new file mode 100644
index 0000000000..283c44fda6
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst
@@ -0,0 +1,5 @@
+- Removed legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath``
+  which were undocumented, broken variants of :cmd:`Add LoadPath`,
+  :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath`
+  (`#11187 <https://github.com/coq/coq/pull/11187>`_,
+  by Maxime Dénès and Théo Zimmermann).
-- 
cgit v1.2.3