The Coq mailing list

[Olivier Boite <boite AT iie.cnam.fr>]

We're actually working on a tactic requiring the exact definition stored in
the coq environment. In particular, we would like to disactivate the
pretty printing feature so that no syntactic replacement is performed. In
fact, we are not directly working on the internal representation provided by
coq but are using the Pp module to obtain the definition.(which will
afterwards be treated by an external lexer and parser).

For instance,  with ZArith,  the term   `x <= x`   should be printed   (Zle x
x).

We would like to know whether this is possible or is there any function
already implemented that can return any particular definition
as a string , without considering printing rules  "Syntax constr level 0: ..."
added at toplevel ?
Thanks,
JF Etienne, O. Boite