From 46c28054eb404175e5ba9485c3b5efbfe1b81619 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 30 Dec 2020 12:39:53 -0800 Subject: Deprecate "at ... with ..." in change tactic (use "with ... at ..." instead) --- doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst | 7 +++++++ doc/sphinx/proofs/writing-proofs/rewriting.rst | 3 +++ 2 files changed, 10 insertions(+) create mode 100644 doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst new file mode 100644 index 0000000000..306fe8052d --- /dev/null +++ b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst @@ -0,0 +1,7 @@ +- **Deprecated:** + In :tacn:`change` and :tacn:`change_no_check`, the + `at ... with ...` form is deprecated. Use + `with ... at ...` instead. For `at ... with ... in H |-`, + use `with ... in H at ... |-`. + (`#13696 `_, + by Jim Fehrle). 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 -- cgit v1.2.3