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