The refman states (in the Module part):
When Coq is processing a script that hasn't been saved in a file, such as a new buffer in CoqIDE or anything in coqtop, definitions in the script are associated with the logical name Top and there is no associated file system path.
Indeed it works in coqtop. Could it also work in a modified buffer? I'm thinking of Search _ in Top
which would be so nice.
if the modified buffer was saved, that wouldn't work easily
a saved script foo.v
can refer to its definitions via its own name foo
in some cases, which would break if the name were Top
but why not use the real name?
To be honest here, I'm merely trying to see if this part of the refman is still relevant. But I was also looking for a command to check everything from the top of the current file and I had a tiny hope this could be used.
there's Print All although it doesn't support filtering and doesn't print the content of finished modules
Last updated: Oct 13 2024 at 01:02 UTC