From 75f93e90e95f049ae23023f39add16a861ae114b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 26 Apr 2019 13:00:38 +0200
Subject: [ssr] under: extend ssreflect.v to generalize iff to any setoid eq

* Add an extra test with an Equivalence.

* Update the doc accordingly.
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ed980bd4de..0af23354cc 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,8 +3756,9 @@ involves the following steps:
    the corresponding intro pattern :n:`@i_pattern__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
-   are (quantified) equalities or double implications between a
-   term and an evar (e.g. ``m - m = ?F2 m`` in the running example).
+   are (quantified) Leibniz equalities or registered Setoid equalities
+   between a term and an evar (e.g. ``m - m = ?F2 m`` in the running
+   example).
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
-- 
cgit v1.2.3