From d4e07328f7aed9d19e9b9a0f442e8fe85643073a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 6 Aug 2019 23:34:07 +0200 Subject: [doc][ssr][under][setoid] Add changelog entry --- doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/05-tactic-language/10022-ssr-under-setoid.rst 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 `_, + by Erik Martin-Dorel, with suggestions and review by Enrico Tassi). -- cgit v1.2.3