The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Without delving into OCaml, is it possible to write my own "pretty-printing" routine in Coq?

  What I mean is as follows: when looking at the goal state, besides toggling certain options, I have absolutely no control over how the Hypothesis and Conclusion is displayed.

  For complicated situations (a Record containing a list of other Records), I would like to have a bit more control over what is displayed and what is not displayed.

  Basically, I want to be able to write a function of type (Gallina Term -> list string).

  I'm also using proof general. If others have run into this problem and found that hacking at the elisp layer to rewrite the buffer, advice from that would be helpful too.

Thanks!