From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p1PAD2me018015 for ; Fri, 25 Feb 2011 11:13:02 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Al0CAHoPZ02EpqxrmWdsb2JhbACYKI4SFQEBAQEBCAsKBxElvQWFYAQ X-IronPort-AV: E=Sophos;i="4.62,224,1297033200"; d="scan'208";a="92069982" Received: from sainfoin-out.extra.cea.fr ([132.166.172.107]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 25 Feb 2011 11:12:57 +0100 Received: from pisaure.intra.cea.fr (pisaure.intra.cea.fr [132.166.88.21]) by sainfoin.extra.cea.fr (8.14.2/8.14.2/CEAnet-Internet-out-2.0) with ESMTP id p1PACvfm016724 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Fri, 25 Feb 2011 11:12:57 +0100 Received: from muguet1.intra.cea.fr (muguet1.intra.cea.fr [132.166.192.6]) by pisaure.intra.cea.fr (8.14.4/8.14.4) with ESMTP id p1PACuIc025894 for ; Fri, 25 Feb 2011 11:12:57 +0100 (envelope-from paolo.herms@cea.fr) Received: from is010237.localnet (is005060.intra.cea.fr [132.166.135.160]) by muguet1.intra.cea.fr (8.13.8/8.13.8/CEAnet-Intranet-out-1.1) with ESMTP id p1PACuZk003592 for ; Fri, 25 Feb 2011 11:12:56 +0100 From: Paolo Herms To: caml-list@inria.fr Date: Fri, 25 Feb 2011 11:12:55 +0100 User-Agent: KMail/1.13.6 (Linux/2.6.37-ARCH; KDE/4.6.0; x86_64; ; ) References: <1962615140.235442.1298625990054.JavaMail.root@zmbs3.inria.fr> In-Reply-To: <1962615140.235442.1298625990054.JavaMail.root@zmbs3.inria.fr> MIME-Version: 1.0 Content-Type: Text/Plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Message-Id: <201102251112.56387.paolo.herms@cea.fr> Subject: Re: [Caml-list] type constructor polymorphism On Friday 25 February 2011 10:26:30 Damien Pous wrote: > How would you translate the following (pseudo)Coq code ? > [...] using Recursive Extraction map_one map_two map_many. Seriously, why not have Coq extracted parts of your library? It may use some magic here and there but you can be sure it's what you wanted. You just have to make sure you don't call functions like your k directly from caml code but through Coq extracted wrappers whose types are also in ml, like your map functions. -- Paolo Herms PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project Paris, France