- **Removed:**
  Remove decimal-only number notations which were deprecated in 8.12.
  (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux).