Fix #18657: "Include" objects were not always taken into account in Search

doc/changelog/08-vernac-commands-and-options/18662-master+small-cleanup-declare_variable.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  :cmd:`Search` now searches also in included module types
+  (`#18662 <https://github.com/coq/coq/pull/18662>`_,
+  fixes `#18657 <https://github.com/coq/coq/issues/18657>`_,
+  by Hugo Herbelin).

test-suite/output/bug_18657.out

@@ -0,0 +1,12 @@
+bar_1: bar = 1
+First.bar_1: First.bar = 1
+bar: nat
+First.bar: nat
+First.bar_1: First.bar = 1
+bar_1: bar = 1
+bar_1: bar = 1
+bar_1: bar = 1
+one_bar: 1 = bar
+baz_foo: baz tt = foo
+baz: unit -> t
+baz_foo: baz tt = foo

test-suite/output/bug_18657.v

@@ -0,0 +1,42 @@
+Module First.
+  Definition bar := 1.
+  Lemma bar_1 : bar = 1. Proof. reflexivity. Qed.
+End First.
+
+Module Import Second.
+  Include First.
+  Search bar. (*First.bar_1: First.bar = 1*)
+  Search "bar".
+  Lemma one_bar : 1 = bar. Proof. rewrite bar_1. reflexivity. Qed.
+End Second.
+
+Module Type B.
+  Definition bar := 1.
+  Lemma bar_1 : bar = 1. Proof. reflexivity. Qed.
+End B.
+
+Module A.
+  Include B.
+  Search bar. (* was nothing *)
+  Lemma one_bar : 1 = bar. Proof. rewrite bar_1; reflexivity. Qed.
+  Search bar. (* was only one_bar *)
+End A.
+
+Module Type HasFoo.
+  Parameter t : Type.
+  Parameter foo : t.
+End HasFoo.
+
+Module MakeBaz (Import M : HasFoo).
+  Definition baz := fun (_ : unit) => foo.
+  Lemma baz_foo : baz tt = foo. Proof. reflexivity. Qed.
+End MakeBaz.
+
+Module Import Baz <: HasFoo.
+  Definition t := nat.
+  Definition foo := 42.
+  Include MakeBaz.
+  Search baz. (* was nothing *)
+  Search "baz". (* was nothing *)
+  Lemma foo_bas : foo = baz tt. Proof. rewrite baz_foo. reflexivity. Qed.
+End Baz.

vernac/declaremods.ml

@@ -1603,7 +1603,7 @@ let iter_all_interp_segments f =
     List.iter (apply_obj prefix) modobjs.module_substituted_objects;
     List.iter (apply_obj prefix) modobjs.module_keep_objects
   in
-  let apply_nodes (node, os) = List.iter (fun o -> f (Lib.node_prefix node) o) os in
+  let apply_nodes (node, os) = List.iter (fun o -> apply_obj (Lib.node_prefix node) o) os in
   MPmap.iter apply_mod_obj (InterpVisitor.ModObjs.all ());
   List.iter apply_nodes (Lib.contents ())