From f7c078d1a16a9554fb320a85b4c7d33499037484 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Nov 2019 01:59:07 +0100
Subject: [ssr] Update doc for under w.r.t. setoid-like relations

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 3db771b0ba..e70f9d7716 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3757,8 +3757,10 @@ involves the following steps:
 
 4. Then :tacn:`under` checks that the first n subgoals
    are (quantified) Leibniz equalities, double implications or
-   registered Setoid equalities between a term and an evar
-   (e.g. ``m - m = ?F2 m`` in the running example).
+   registered relations (w.r.t. Class ``RewriteRelation``) between a
+   term and an evar, e.g. ``m - m = ?F2 m`` in the running example.
+   (This support for setoid-like relations is enabled as soon as we do
+   both ``Require Import ssreflect.`` and ``Require Setoid.``)
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
@@ -3770,7 +3772,10 @@ involves the following steps:
    by using a regular :tacn:`rewrite` tactic.
 
 7. Interactive editing of the first n goals has to be signalled by
-   using the :tacn:`over` tactic or rewrite rule (see below).
+   using the :tacn:`over` tactic or rewrite rule (see below), which
+   requires that the underlying relation is reflexive. (The running
+   example deals with Leibniz equality, but ``PreOrder`` relations are
+   also supported, for example.)
 
 8. Finally, a post-processing step is performed in the main goal
    to keep the name(s) for the bound variables chosen by the user in
@@ -3796,6 +3801,10 @@ displayed as ``'Under[ … ]``):
    This is a variant of :tacn:`over` in order to close ``'Under[ … ]``
    goals, relying on the ``over`` rewrite rule.
 
+Note that a rewrite rule ``UnderE`` is available as well, if one wants
+to "unprotect" the evar, without closing the goal automatically (e.g.,
+to instantiate it manually with another rule than reflexivity).
+
 .. _under_one_liner:
 
 One-liner mode
-- 
cgit v1.2.3