In the Coq script below: why does Search "foo" inside Foo2 not find anything? I expected it to find foo, since foo at that point in the script is part of the current context. Is there some way to make foo visible to the Search command?
Module Type MT.
Parameter f : nat -> nat -> Prop.
Parameter f_thm : forall x, f x x.
End MT.
(* prints nothing, as expected: *)
Search "f_thm".
Module Foo (mt : MT).
(* prints: mt.f_thm: forall x : nat, mt.f x x *)
Search "f_thm".
Lemma foo : 1 + 1 = 2. Proof. reflexivity. Qed.
(* prints: foo: 1 + 1 = 2 *)
Search "foo".
End Foo.
(* prints nothing, as expected: *)
Search "foo".
Module Foo2 (mt : MT).
Include (Foo mt).
(* prints nothing, unexpected: *)
Search "foo".
End Foo2.
This was a bug, fixed in the current development version of Coq (8.20+alpha).
See https://github.com/coq/coq/issues/18657 for the issue and https://github.com/coq/coq/pull/18662 for the fix.