- **Removed:** Removed info tactic that was deprecated in 8.5.
  (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle).