coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Claudio Sacerdoti Coen <sacerdot AT CS.UniBO.IT>
- To: coq-club AT pauillac.inria.fr, veronique.benzaken AT lri.fr, Giuseppe.Castagna AT ens.fr, frisch AT clipper.ens.fr, Marwan.Burelle AT lri.fr
- Subject: Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.
- Date: Tue, 11 Feb 2003 16:47:58 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear Serge,
On Tue, Feb 11, 2003 at 15:05:08 +0100, Serge Leblanc wrote:
> Hello, for my first contribution I wish to
> carry out a Coq->CDuce[1] extraction functionality.
what do you want to extract exactly?
> Before starting I would like to know if somebody does not
> already carry out this.
Depending on what do you want to extract, it may be a good
idea to either:
1. start from the extracted XML files.
[The extraction module to XML is already part of the standard
distribution of Coq, but it is undocumented. (Some small
parts will change again in a few monthes. Other are really
stable.) Feel free to ask me more infos about that.]
2. modify the extraction module for XML files.
[More difficult than 1, IMHO.]
3. restart from scratch if the information you need is not there.
[In this case I would be interested in privately know what
is the missing information.]
Regards,
C.S.C.
--
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
PhD Student in Computer Science at University of Bologna
E-mail:
sacerdot AT cs.unibo.it
http://caristudenti.cs.unibo.it/~sacerdot
----------------------------------------------------------------
- [Coq-Club] Build an Coq-CDuce extraction functionnality., Serge Leblanc
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Claudio Sacerdoti Coen
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Veronique Benzaken
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Giuseppe Castagna
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Pierre Letouzey
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Serge Leblanc
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Giuseppe Castagna
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Pierre Letouzey
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Claudio Sacerdoti Coen
Archive powered by MhonArc 2.6.16.