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
---
 vernac/g_vernac.mlg | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'vernac')

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