New to Coq, working through Software Foundations. Just discovered the Search command, but it will match anything in the current environment, whereas I really just want to search what things I've proven in the current module (i.e. not anything that's been imported). Something like Search plus inside .. (where '.' would mean "current module only").
I could just exclude every other module, but that's painful.
As shown by the reference manual documentation, there is no variant of Search doing exactly what you ask.
However, here are 3 approaches that you can follow to address this use case—search what things were proven in the current module:
First, assuming you are developing material in an explicit module, you can temporarily close this module (i.e., End module.) and use Search "…" inside module.
Full example:
Module module.
(* … *) Definition natty := 21. (* … *)
End module. Search "nat" inside module.
If you don't use interactives modules, you can still blacklist the identifiers that appear in the standard library (or other libraries) by specifying a common identifier (e.g., Coq.)
Full example:
Definition natty := 21. (* … *)
Add Search Blacklist "Coq.". Search "nat".
Finally if you are not interested in a fine-grained search of patterns/types, but would just want to print what things were defined/proven in the current module, you can use this command:
Definition natty := 21. (* … *)
Print All.