I am to run Coq scripts. I loaded a file into Coq IDE but it stops at using an identifier defined in another .v file.
The first file imports the second via
Should I do something special so that Coq IDE would load the second .v file and recognize that identifier.
Should I first run that second file through Coq and save a compiled version of it?
CoqIDE needs files that you load to be already compiled to
.vo format. This can be accomplished directly via
coqc or indirectly via
coq_makefile for the file you need to load.
I compiled the dependency file into .vo object file with coqc.
Still, when I open the first file I stuck at an identifier that is from the dependency file.
What did I miss?
Last updated: Jan 28 2023 at 06:30 UTC