diff options
Diffstat (limited to 'doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst')
| -rw-r--r-- | doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst index 5e005742fd..424540b46a 100644 --- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst +++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst @@ -1,4 +1,5 @@ -- Generalize tactics :tacn:`under` and :tacn:`over` for any registered +- **Added:** + Generalize tactics :tacn:`under` and :tacn:`over` for any registered relation. More precisely, assume the given context lemma has type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The first step performed by :tacn:`under` (since Coq 8.10) amounts to |