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?