blob: e9f51461e54990b8c46cf934b1882e98de56e35c (
plain)
1
2
3
4
5
|
- **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).
|
