Merge PR #12537: Take into account the existing delta-resolver when starting a new interactive module or module type

Reviewed-by: SkySkimmer

4 files changed, 38 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).
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 93337fca5d..8b85072d6d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1023,6 +1023,8 @@ let start_module l senv =
   mp,
   { empty_environment with
     env = senv.env;
+    modresolver = senv.modresolver;
+    paramresolver = senv.paramresolver;
     modpath = mp;
     modvariant = STRUCT ([],senv);
     required = senv.required }
@@ -1034,6 +1036,8 @@ let start_modtype l senv =
   mp,
   { empty_environment with
     env = senv.env;
+    modresolver = senv.modresolver;
+    paramresolver = senv.paramresolver;
     modpath = mp;
     modvariant = SIG ([], senv);
     required = senv.required }
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 317e9c3757..09feca71e7 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -455,3 +455,6 @@ PreOrder_Reflexive:
 reflexive_eq_dom_reflexive:
   forall {A B : Type} {R' : Relation_Definitions.relation B},
   Reflexive R' -> Reflexive (eq ==> R')%signature
+B.b: B.a
+A.b: A.a
+F.L: F.P 0
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 4ec7a760b9..a5ac2cb511 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -66,3 +66,26 @@ Reset Initial.
 Require Import Morphisms.
 
 Search is:Instance [ Reflexive | Symmetric ].
+
+Module Bug12525.
+  (* This was revealing a kernel bug with delta-resolution *)
+  Module A. Axiom a:Prop. Axiom b:a. End A.
+  Module B. Include A. End B.
+  Module M.
+    Search B.a.
+  End M.
+End Bug12525.
+
+From Coq Require Lia.
+
+Module Bug12647.
+  (* Similar to #12525 *)
+  Module Type Foo.
+  Axiom P : nat -> Prop.
+  Axiom L : P 0.
+  End Foo.
+
+  Module Bar (F : Foo).
+  Search F.P.
+  End Bar.
+End Bug12647.