I can't load modules that are in same folder in CoqIde.
I'm trying to load sources from Software Foundations, I'm running coqide in folder that contains SF sources with coqide
or coqide ./
, then after opening and running the file, I'm getting this error:
Error: Cannot find library Poly in loadpath
in this line:
Require Export Poly.
and it's same for every other require
commands.
So how are you people loading programs from SF into coqide ?
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With