diff options
| author | Pierre-Marie Pédrot | 2020-11-20 13:20:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-20 13:20:18 +0100 |
| commit | 04186f83545e3c693976c73d488b36dd4a2b50db (patch) | |
| tree | 7f22af1415d31b515f8ea4ed42e356279d2756f6 /doc/sphinx/proofs | |
| parent | 1fd6af1ae6d4a46547cdd2bf812ef46e0727138f (diff) | |
| parent | 6adbb8b2c055820777721eae9a3409f9067a8d0e (diff) | |
Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 8 |
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 31050cb107..5283f60b11 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 |