The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

I'd be interested in the same information...
--- nadeem


Robert R. Schneck wrote:

> 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