- **Fixed:** Notations understand universe names without getting
  confused by different imported modules between declaration and use
  locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes
  `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan
  Gilbert).