coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Serge Leblanc <serge.leblanc AT wanadoo.fr>
- To: coq-club AT pauillac.inria.fr
- Cc: veronique.benzaken AT lri.fr, Giuseppe.Castagna AT ens.fr, frisch AT clipper.ens.fr, Marwan.Burelle AT lri.fr
- Subject: [Coq-Club] Build an Coq-CDuce extraction functionnality.
- Date: Tue, 11 Feb 2003 15:05:08 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello, for my first contribution I wish to
carry out a Coq->CDuce[1] extraction functionality.
Before starting I would like to know if somebody does not
already carry out this.
I would not wish to waste my time to remake an already existing
functionality.
[1] http://www.cduce.org/
--
Serge Leblanc
110 rue de charnècles
38340 Voreppe
tél: 06 23 22 55 58
GnuPG Key ID : 73791C2B
GnuPG Key fingerprint = 8817 E63A 82D4 EFE9 E28B FDFE C9F6 6104 19A9 BFA6
- [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.