coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Machine-parseable format for Coq terms

From: Stéphane Glondu <steph AT glondu.net>
To: "Edward Z. Yang" <ezyang AT mit.edu>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Machine-parseable format for Coq terms
Date: Fri, 06 Apr 2012 17:12:11 +0200

Le 05/04/2012 17:51, Edward Z. Yang a écrit :
> Is there a way to access, say, hypotheses in an in-progress proof,
> or the goals, and pass them to the Print XML facility? (Think of:
> domain specific proof general application)

Maybe you are looking for "external", documented in chapter "The tactic
language"?

Cheers,

--
Stéphane

[Coq-Club] Machine-parseable format for Coq terms, Edward Z. Yang
- Re: [Coq-Club] Machine-parseable format for Coq terms, Stéphane Glondu
  - Re: [Coq-Club] Machine-parseable format for Coq terms, Edward Z. Yang
    - Re: [Coq-Club] Machine-parseable format for Coq terms, Stéphane Glondu