The Coq mailing list

["Robert R. Schneck" <schneck AT Math.Berkeley.EDU>]

I'm working on a project in which it would be convenient to interface
directly with the Coq source code to produce and type-check Coq terms.
Basically it seems to me that I need
 * a type of (well-formed) constructions
 * a function which, given two constructions, checks whether
     the typing judgement holds between them
all of which I suppose must happen in the context of an
 * environment of declarations and definitions

And I'll want a very simple parser and pretty-printer for terms.

Could anyone help me to find these entities in the source?

Many thanks.
Robert