[doc] warn that (automatic) clears can result in errors

1 files changed, 10 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7c597d3ffa..483dbd311d 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1445,6 +1445,16 @@ section constant.
 If tactic is ``move`` or ``case`` and an equation :token:`ident` is given, then clear
 (step 3) for :token:`d_item` is suppressed (see section :ref:`generation_of_equations_ssr`).
 
+Intro patterns (see section :ref:`introduction_ssr`)
+and the ``rewrite`` tactic (see section :ref:`rewriting_ssr`)
+let one place a :token:`clear_switch` in the middle of other items
+(namely identifiers, views and rewrite rules).  This can trigger the
+addition of proof context items to the ones being explicitly
+cleared, and in turn this can result in clear errors (e.g. if the
+context item automatically added occurs in the goal).  The
+relevant sections describe ways to avoid the unintended clear of
+context items.
+
 
 Matching for apply and exact
 ````````````````````````````