aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/03-notations/13842-remove-decimal.rst
blob: 4bc26ef6a86998157caac6e1d3c666a45ca5f077 (plain) 
1
2
3

- **Removed:**
  Remove decimal-only number notations which were deprecated in 8.12.
  (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:22:46 +0000