Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Howto: AST -> constr ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Howto: AST -> constr ?


chronological Thread 
  • From: Piotr Ko�bia� <pk174340 AT zodiac.mimuw.edu.pl>
  • To: "Coq-Club" <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Howto: AST -> constr ?
  • Date: Sun, 26 Oct 2003 23:36:02 +0100
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello!

I'm a new member of the list.
I have a question about primitive pretty-printers written in ML. I'm using
Coq 7.3.1. I know I have to write a function of type 'Esyntax.std_printer',
and that is 'Coqast.t->std_ppcmds'. I do not fully understand the 'Coqast.t'
type and anyway my printer only has to print terms. So my question is, is
there an easy way to change (interpret) 'Coqast.t' into 'constr'?

Piotr Kozbial





Archive powered by MhonArc 2.6.16.

Top of Page