Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq syntax to XML

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq syntax to XML


Chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Coq syntax to XML
  • Date: Wed, 8 Oct 2014 19:06:22 -0700
  • Importance: Normal

I'm told that Coq 8.5 is going to support conversion of Coq syntax to XML.  Can someone give me more information on what is planned?  I am in the process of developing a UI for Coq.  A couple of items that would be nice is if this conversion 1) Saved line/character information in the original Coq source and 2) would be able to parse the goal/hypothesis status information that is printed after a proof tactic is applied.

                    - Ken



Archive powered by MHonArc 2.6.18.

Top of Page