The Coq mailing list

[Julien Thierry <thierry AT adacore.com>]

Dear Coq-Club,

First, I have two problems to report:
- When I try to use the command "Show XML Proof.", I always
  get the message: 
  "Anomaly: Xmlcommand.show_pftreestate is not supported in this version..
   Please report."
  This problem occurs whether or not I set the COQ_XML_LIBRARY_ROOT
variable.
- When I use the command "coqc -xml test.v"(or coqtop -xml test.v) and the
COQ_XML_LIBRARY_ROOT
  is set I get this message: 
  "Uncaught exception: End_of_file
   Anomaly: Error executing "/pathtocoqinstall/bin/coqdoc --html -s
--body-only --no-index --latin1 --raw-comments -o
/pathinCOQ_XML_LIBRARY_ROOT/test.theory.xml
/pathinCOQ_XML_LIBRARY_ROOT/test.theory.v".
   Please report."

I joined an exemple where those errors occur. I tried with the version
8.4pl3 and
with a fresh clone of coq's git. Both version are compiled for Linux.


Also, I was wondering, is there a way to recover the vernac files from the
exported XML files?

Best regards,

-- 
Julien Thierry
Require Import Zorder.
Require Import BinInt.

Theorem testing : (0 <= 1)%Z.
Proof.
  apply Zle_0_1.
Qed.