The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I've downloaded the String definition from the Coq website 
(http://coq.inria.fr/contribs/String.html), but I'm getting compiler errors.  
The package contains no real information about compiling it, and I am at a 
bit of a loss as to how to troubleshoot this.  Can someone provide some help?

Thanks
Rob Dockins


The error message follows:

$ coqc -v
The Coq Proof Assistant, version 8.0pl3 (Jan 2006)
compiled on Feb 08 2006 04:00:21

$ camlp4 -v
Camlp4 version 3.08.3

$ ocamlc -v
The Objective Caml compiler, version 3.08.3
Standard library directory: /usr/lib/ocaml

$ make
ocamlc -c  -I . -I /kernel -I /lib -I /library -I /parsing -I /pretyping 
-I /interp -I /proofs -I /syntax -I /tactics -I /toplevel 
-I /contrib/correctness -I /contrib/extraction -I /contrib/field 
-I /contrib/fourier -I /contrib/graphs -I /contrib/interface 
-I /contrib/jprover -I /contrib/omega -I /contrib/romega -I /contrib/ring 
-I /contrib/xml -I `camlp4 -where` -pp "camlp4o -I . -I /parsing 
pa_extend.cmo pa_ifdef.cmo q_MLast.cmo grammar.cma -impl" g_ascii_syntax.ml
Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead.
Error while loading "grammar.cma": file not found in path.
Preprocessor error
make: *** [g_ascii_syntax.cmo] Error 2