The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> I have a question concerning the XML output function of Coq:
> 
> I'd like to have a local copy of the Coq standard library in XML. Is 
> there a quick way to get this? For example, can I create the XML library 
> already when compiling Coq, by patching the make file ?

Explanations are in the Reference Manual (see
e.g. http://coq.inria.fr/doc/Reference-Manual018.html#toc94).

> when trying coqc -xml on some theory file of Coq's standard library 
> (here Datatypes.v), I get the error "Name Coq.Init starts with prefix 
> "Coq" which is reserved for the Coq library". Since the Coq library is 
> precisely what I want, how can I proceed here ?

In this situation, you need to use option -boot (and, for Init, the
extra option -nois) as in "bin/coqtop -boot -xml -nois -compile Datatypes".

Good luck,

Hugo Herbelin