The Coq mailing list

["Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>]

> >Could anyone help me to find these entities in the source?
> >Robert
> I'd be interested in the same information...
> --- nadeem

I recently had to do that too (the code has pretty changed in the last 5
years... :-).

I think it would be nice if the Coq team could include
a short description of  "the Coq API" as part of the official documentation
of the system.  This API would contain information
from the .mli files for selected functions that could be "entry points" to
interface
Coq's code with other tools. The functions mentioned by Robert are some
examples of such functions. Better: all that could be pretty packaged in a
few
Ocaml modules ready to be imported and used :-). This should not be too
expensive,
since the information already exists in the Coq sources and is formatted to
generate
html documentation pages in the style of  JavaDoc.

Best,
Eduardo.

----- Original Message -----
From: "Nadeem Abdul Hamid" 
<nadeem AT acm.org>
Cc: 
<coq-club AT pauillac.inria.fr>
Sent: Monday, March 17, 2003 4:26 PM
Subject: Re: [Coq-Club] working with the Coq source code


> 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
> >
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>