The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Vladimir Voevodsky wrote:
> A related question: does Cow has an "internal representation" language 
> with a more rigid syntactic structure?

Like pretty much all tools that process programming languages, Coq uses 
abstract syntax trees internally.  As far as I know, the "format" isn't 
documented, but you can see it in the source code.  The Coq 
implementation is pretty modular, so it's not actually that much trouble 
to write (and dynamically load) your own modules that manipulate syntax 
trees.  You just need to learn the "API details" by reading .mli files 
in the source.