diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst new file mode 100644 index 0000000000..bec121836c --- /dev/null +++ b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst @@ -0,0 +1,8 @@ +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 + <https://github.com/coq/coq/pull/12525>`_ and `#12647 + <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). |