diff options
| author | Jim Fehrle | 2020-12-30 12:39:53 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-02 22:34:15 -0800 |
| commit | 46c28054eb404175e5ba9485c3b5efbfe1b81619 (patch) | |
| tree | bc333811872b07448b765481b7fab486aeb97323 /doc/sphinx | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Deprecate "at ... with ..." in change tactic
(use "with ... at ..." instead)
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 07b7928847..8873d02888 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -280,6 +280,9 @@ Rewriting with definitional equality whose value which will substituted for `x` in :n:`@one_term__to`, such as in `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`. + The `at ... with ...` form is deprecated in 8.14; use `with ... at ...` instead. + For `at ... with ... in H |-`, use `with ... in H at ... |-`. + :n:`@occurrences` If `with` is not specified, :n:`@occurrences` must only specify entire hypotheses and/or the goal; it must not include any |