The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Claudia Fernanda Oliveira K Tavares writes:
 > 
 >  I had some problems because it has a dependency between the files and I 
 > don't get to compile the files:
 > 
 > - But when a try to load the "theta.v" module, it causes an error: 
 >             Coq < Load theta. 
 >             Error while reading /home/consiste/claudia/Programas/coq- 
 >             8.0/theories/blinc/theta/theta.v : 
 >             File "/home/consiste/claudia/Programas/coq- 
 >             8.0/theories/blinc/theta/theta.v", line 1, characters 8-13 
 >             User error: Cannot find library claus in loadpath 

The message "Cannot find library claus" indicates that Coq is looking
for a compiled version of claus.v, that is claus.vo, when interpreting
a command such as "Require claus". So you probably forgot to compile
claus.v first.

-- 
Jean-Christophe