diff options
| author | Erik Martin-Dorel | 2019-08-06 23:34:07 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-08-08 11:11:54 +0200 |
| commit | d4e07328f7aed9d19e9b9a0f442e8fe85643073a (patch) | |
| tree | 126508ec26b3cd4fd4072fd689ed5366596c3a4c | |
| parent | 05ae4be1258ed198949f886e83151fb41f7dedb1 (diff) | |
[doc][ssr][under][setoid] Add changelog entry
| -rw-r--r-- | doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst b/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst new file mode 100644 index 0000000000..00b988ed4c --- /dev/null +++ b/doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst @@ -0,0 +1,6 @@ +- The :tacn:`under` and :tacn:`over` tactics can handle any registered + setoid equality (beyond mere double implications). See also Section + :ref:`under_ssr`. This generalized support for setoid equalities is + enabled as soon as we do both ``Require Import ssreflect.`` and + ``Require Setoid.`` (`#10022 <https://github.com/coq/coq/pull/10022>`_, + by Erik Martin-Dorel, with suggestions and review by Enrico Tassi). |