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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

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";
-- 
cgit v1.2.3