diff options
| author | Enrico Tassi | 2020-01-03 19:09:15 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-01-03 19:09:15 +0100 |
| commit | 793bddef6b4f615297e9f9088cd0b603c56b2014 (patch) | |
| tree | bff9cb13225836a72ebed11044636204b7537eb3 /doc | |
| parent | fbd911ee701a63a05c213cfe6e98271fa54c874a (diff) | |
| parent | c380202139b158647089c1352bcacf82c99012ea (diff) | |
Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issue
Reviewed-by: gares
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/changes.rst | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1d0c937792..33fc211fa5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -350,11 +350,8 @@ Changes in 8.11+beta1 `iff`. Now, it is also performed for any relation `R1` which has a ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` - goal by instantiating the hidden evar.) Also, it is now possible to - manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` - is a `PreOrder` relation or so, thanks to extra instances proving - that `Under_rel` preserves the properties of the `R1` relation. - These two features generalizing support for setoid-like relations is + goal by instantiating the hidden evar.) + This feature generalizing support for setoid-like relations is enabled as soon as we do both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been added if one wants to "unprotect" the evar, and instantiate it |