concerning Coq XML output

[Benedikt.AHRENS]

Hello,

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 ?

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 ?

Greetings
ben

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[hugo.herbelin]

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club