Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

coqide - can't load modules from same folder

Tags:

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 ?