diff options
| author | Erik Martin-Dorel | 2019-12-27 01:32:58 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-12-27 01:32:58 +0100 |
| commit | c380202139b158647089c1352bcacf82c99012ea (patch) | |
| tree | 0fe8f21baed7f4680e30045c4ec22c3110ebad77 | |
| parent | ec2d1bc0d0f0447f8824def545697b8c05fcb670 (diff) | |
docs: Update changes.rst w.r.t. ssrsetoid.v's simplification
| -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 |