From ca0002823429a6c7de953446b6d351332d24daa7 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 12 May 2020 11:56:39 +0200
Subject: Changelog entries for #8855.

---
 .../06-ssreflect/8855-master+more-search-options.rst          | 11 +++++++++++
 .../8855-master+more-search-options.rst                       |  9 +++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 doc/changelog/06-ssreflect/8855-master+more-search-options.rst
 create mode 100644 doc/changelog/07-commands-and-options/8855-master+more-search-options.rst

(limited to 'doc')

diff --git a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
new file mode 100644
index 0000000000..2fdacfd82a
--- /dev/null
+++ b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
@@ -0,0 +1,11 @@
+- **Changed:** The :cmd:`Search (ssreflect)` command that used to be
+  available when loading the `ssreflect` plugin has been moved to a
+  separate plugin that needs to be loaded separately: `ssrsearch`
+  (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes
+  `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo
+  Zimmermann).
+
+- **Deprecated:** :cmd:`Search (ssreflect)` (available through
+  `Require ssrsearch.`) in favor of the `headconcl:` clause of
+  :cmd:`Search` (part of `#8855
+  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
new file mode 100644
index 0000000000..cd993bf356
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
@@ -0,0 +1,9 @@
+- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`,
+  `headconcl:`, `head:` and `is:` in :cmd:`Search`.  Support for
+  complex search queries combining disjunctions, conjunctions and
+  negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo
+  Herbelin, with ideas from Cyril Cohen and help from Théo
+  Zimmermann).
+- **Deprecated:** :cmd:`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).
-- 
cgit v1.2.3