In sort of the same vein, in Coq, we have named hypotheses in our
proof contexts which render like:

  Hyp0 : Hyp (P x)
  Hyp1 : Hyp (P z)
   or (P x) (or (forall y : U, P y) False)

I'd like to add some PGML so that it looks something like this:

      <hyp>Hyp0 : Hyp (P x)</hyp>
      <hyp>Hyp1 : Hyp (P z)</hyp>
      or (P x) (or (forall y : U, P y) False)

But I don't know what the right PGIP/PGML tags are.


Excerpts from Edward Z. Yang's message of Thu Apr 05 23:15:50 -0400 2012:
> Hello all,
> I'm working on partial PGIP support Coq, and one thing that I would like
> to support is the case when Coq outputs "warning" messages, of which
> there are many but which are nonfatal.  I'm wondering what the right
> tag for these are.  <errorresponse> is not correct, because we're only
> allowed to have one before <ready/>.  Is <metainforesponse> correct?
> It seems too generic, and where am I supposed to attach other metadata?
> Cheers,
> Edward
ProofGeneral-devel mailing list

Reply via email to