diff options
| author | Gaëtan Gilbert | 2020-07-10 13:07:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-10 13:07:21 +0200 |
| commit | f2dc2f5fc8c745c69c0161a91063b11838fb684b (patch) | |
| tree | 0127fb4a562a4a56af12a4bef332705562996f2d /doc | |
| parent | 9b4d89c5376e8018ca94bc3bd877f99f1d03ec74 (diff) | |
| parent | 0046a166843495b131fb197788c28de9b4705685 (diff) | |
Merge PR #12537: Take into account the existing delta-resolver when starting a new interactive module or module type
Reviewed-by: SkySkimmer
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). |