diff options
| author | coqbot-app[bot] | 2021-01-28 14:37:10 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-28 14:37:10 +0000 |
| commit | a54a5b83becd3ef7feef1352b56d10a3d74be85f (patch) | |
| tree | 30fd0b947b44f92a567eb7e7ce9c27706f5c3c9d /doc/sphinx/changes.rst | |
| parent | 90b79076305d8b9ceb92f81a99bf0a9d423903ee (diff) | |
| parent | 3d46bed76e656d6a0e4d87320e4d0fd67d1211c2 (diff) | |
Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 58444e8e82..4769636ae8 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:** |