- **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 <https://github.com/coq/coq/pull/13696>`_,
  by Jim Fehrle).