Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.

Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>

1 files changed, 6 insertions, 2 deletions

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index f3f69a2fdc..3fe9fce8f5 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       .. exn:: Too few occurrences.
          :undocumented:
 
-   .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident
+   .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences
 
-      This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`.
+      In the presence of :n:`with`, this applies :tacn:`change` to the
+      occurrences specified by :n:`@goal_occurrences`. In the
+      absence of :n:`with`, :n:`@goal_occurrences` is expected to
+      only list hypotheses (and optionally the conclusion) without
+      specifying occurrences (i.e. no :n:`at` clause).
 
    .. tacv:: now_show @term