The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi,

if I want to browse library files, I just dump a corresponding
_CoqProject file into the toplevel directory of the library. In the case
of the Standard Library this file would just contain "-R . Coq" and be
located in the "theories" folder. ProofGeneral picks this up to set the
paths corretly, CoqIDE should do so as well.

Best,
Christian



On 10/02/17 18:08, Anthony Bordg wrote:
> Hi Théo,
> 
> 2017-02-10 17:40 GMT+01:00 Théo Zimmermann 
> <theo.zimmi AT gmail.com
> <mailto:theo.zimmi AT gmail.com>>:
> 
>     When you say "I installed", you mean "I build from source", right? 
> 
> 
> yes, build from the source
>  
> 
>     What configuration options did you use? ./configure -local?
> 
> 
> I used "./configure -local", with no further option.
>  
> 
>     When you say "I tried to process a file", you mean a file from the
>     theories/ folder right?
> 
> 
> yes, a file from the "theories" folder (using CoqIDE)
>  
> 
> 
>     If the answer to all these questions is yes, then I've been
>     observing the same problem when trying to improve some theories
>     files (with Emacs/Proof-General too). I wanted to ask around what
>     this was about but did not get to do it yet. However, not being an
>     expert on these matters, I'm afraid I can't help further.
> 
> 
> 
> 
> 
> -- 
> PhD. Anthony Bordg
> postdoctoral fellow
> Mathematical Institute Charles University
> https://sites.google.com/site/anthonybordg/