The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hello,
I've downloaded the last version of Coq (8.1), unfortunately I am  
unable to compile some files containing the definition of additional  
tactics in ML
The same error remains when I tried to compile Bertot and Balaa's  
contribution (RecursiveDefinition) :
ocamlc -c -g  -I . -I /usr/local/lib/coq8-1/kernel -I  
/usr/local/lib/coq8-1/lib -I /usr/local/lib/coq8-1/library -I  
/usr/local/lib/coq8-1/parsing -I /usr/local/lib/coq8-1/pretyping -I  
/usr/local/lib/coq8-1/interp -I /usr/local/lib/coq8-1/proofs -I  
/usr/local/lib/coq8-1/syntax -I /usr/local/lib/coq8-1/tactics -I  
/usr/local/lib/coq8-1/toplevel -I  
/usr/local/lib/coq8-1/contrib/correctness -I  
/usr/local/lib/coq8-1/contrib/extraction -I  
/usr/local/lib/coq8-1/contrib/field -I  
/usr/local/lib/coq8-1/contrib/fourier -I  
/usr/local/lib/coq8-1/contrib/graphs -I  
/usr/local/lib/coq8-1/contrib/interface -I  
/usr/local/lib/coq8-1/contrib/jprover -I  
/usr/local/lib/coq8-1/contrib/omega -I  
/usr/local/lib/coq8-1/contrib/romega -I  
/usr/local/lib/coq8-1/contrib/ring -I  
/usr/local/lib/coq8-1/contrib/xml -I `camlp4 -where` -pp "camlp4o -I .  
-I /usr/local/lib/coq8-1/parsing pa_extend.cmo pa_ifdef.cmo  
q_MLast.cmo grammar.cma -impl" term_const.ml
Error while loading "grammar.cma": file not found in path.
Preprocessor error
make: *** [term_const.cmo] Erreur 2

I am using the version 3.07 of Ocaml

Thanks in advance for your help

Houda

===============================
         Houda Anoun

    Bordeaux1-LaBRI-Signes
     phone:05 40 00 35 15
  web: www.labri.fr/perso/anoun
        ++++++++++++++
Electric lamps were not invented
    by improving candles
=================================