diff options
| -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). |