The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

I experience issues with the load path in CoqIDE 8.5 (Windows). Specifically 
when I have two files in one directory and run "Compile Buffer" on one file 
and then run the other file, which requires the first one, it sometimes 
works, sometimes it cannot find the compiled files, although they are there. 
This works / doesn't work is for the same pair of files. Does someone 
experience similar problems and could find out when it does work and when it 
doesn't work? I don't set up load paths specifically, but I didn't 
experienced such problems with 8.4pl5 with files in the same folder.

How is the load pat handled by CoqIDE? Does it include the current directory 
of the program and/or the directory of the current file?

Btw.: Is this the right forum for discussing 8.5 issues, or is there a better 
place?

Thanks & best regards,

Michael