The Coq mailing list

["Claudia Fernanda Oliveira K Tavares" <claudia AT consiste.dimap.ufrn.br>]

Hello!

  I've written to Coq Club and some people answered, but I continue with my 
problem. So I'm going to explain better.
  I downloaded one folder called "blinc" that contains many files of module 
type ("filename.v"), I saved in "C:\Coq\lib\theories\blinc" path and I'm 
trying to use in Coq (for Linux and for Windows).
  The resumed hierarchy of files is in this way:
  blinc: claus.v - mcf_thm.v - nnf_thm.v - and other modules (no compiled)
    |_theta: theta.v (no compiled)
    |_newman : newman_assym.v (no compiled)

 I had some problems because it has a dependency between the files and I 
don't get to compile the files:

- I can't test the sample applications because I add the directory "blinc" 
in loadpath: 
           Coq < Add LoadPath "blinc".  
           Coq < Add LoadPath "blinc/theta". 
           Coq < Add LoadPath "blinc/newman". 

- 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 

- So, I try to load the "claus.v" module, it causes an error too: 
            Coq < Load claus. 
            Error while reading /home/consiste/claudia/Programas/coq- 
            8.0/theories/blinc/claus.v : 
            File "/home/consiste/claudia/Programas/coq-   
            8.0/theories/blinc/claus.v", line 3, characters 15-22 
            User error: Cannot find library mcf_thm in loadpath 

- I try to load "mcf_thm" module that require other module and so on... 

  What's wrong? Could anyone help me?

  Regards,

Cláudia.

--
Consiste/DIMAp (http://www.consiste.dimap.ufrn.br/)