diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..9ec568c2c7 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 @@ -319,10 +323,12 @@ Performing computations | delta {? @delta_flag } ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + occs_nums ::= {+ @nat_or_var } + | - {+ @nat_or_var } int_or_var ::= @integer | @ident + nat_or_var ::= @natural + | @ident unfold_occ ::= @reference {? at @occs_nums } pattern_occ ::= @one_term {? at @occs_nums } |