coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Howto: AST -> constr ?, Piotr Ko¼bia³
Archive powered by MhonArc 2.6.16.