From 3d46bed76e656d6a0e4d87320e4d0fd67d1211c2 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 11:55:49 -0800
Subject: Remove the SearchHead command

---
 doc/sphinx/changes.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/changes.rst')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d9e4e4f2b3..b05c6e949c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1301,7 +1301,7 @@ Commands
   Declaration of arbitrary terms as hints. Global references are now
   preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by
   Pierre-Marie Pédrot).
-- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:`
+- **Deprecated:** `SearchHead` in favor of the new `headconcl:`
   clause of :cmd:`Search` (part of `#8855
   <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
 - **Added:**
-- 
cgit v1.2.3