Gergely Buday (Jul 13 2020 at 13:15): Gergely Buday (Jul 13 2020 at 13:15):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
Require Import
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?
Karl Palmskog (Jul 13 2020 at 13:23):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.
Gergely Buday (Jul 13 2020 at 13:25):Thanks
Gergely Buday (Jul 14 2020 at 07:00):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: Sep 23 2023 at 08:01 UTC