diff options
| author | Emilio Jesus Gallego Arias | 2020-05-16 19:21:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-16 19:21:05 +0200 |
| commit | 2b0df4db404a1eb5b149e87ae0d23a5352b18f67 (patch) | |
| tree | 0c127222b11fb7b8a32e1d9835cdc888b024364e /doc/changelog | |
| parent | 05e811a81de90ce698c4f0317d549dc01dc13e17 (diff) | |
| parent | ca0002823429a6c7de953446b6d351332d24daa7 (diff) | |
Merge PR #8855: More search options
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/06-ssreflect/8855-master+more-search-options.rst | 11 | ||||
| -rw-r--r-- | doc/changelog/07-commands-and-options/8855-master+more-search-options.rst | 9 |
2 files changed, 20 insertions, 0 deletions
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). |