The Coq mailing list

[Éric Tanter <etanter AT dcc.uchile.cl>]

Right, thanks. Actually for my needs the better solution was to go directly to OCaml lists:

Extract Inductive list => "list" [ "[]" "(::)" ].

Cheers,

-- Éric

On Jul 23, 2015, at 6:21 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

You should be able to qualify the specific list module that you want and avoid the type issue. In this way, you can still have 'a list, but it should be 'a Coq_module.list instead. 

On Thu, Jul 23, 2015 at 5:12 PM, Éric Tanter <etanter AT dcc.uchile.cl> wrote:

Thanks Robbert -

so the bottom line is: if you spawn ocaml with the .ml file (ocaml -init …), then of course you see the more polymorphic type, but if you first compile with respect to the interface, and then load the compiled module, you get the less general type.

This makes sense.


BTW, I just realized that the compatibility problem I was experiencing has nothing to do with this!! It’s a clash between a new inductive `list’ type that gets extracted from Coq and the native OCaml list type!! Bummer….

-- Éric


> On Jul 23, 2015, at 6:02 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:
>
> On 07/23/2015 10:45 PM, Éric Tanter wrote:
>> I found a very minimal example that makes my point (I’m in Coq 8.5beta2):
>>
>> Test.v
>> --------
>> Require Import String ExtrOcamlString.
>> Extraction "append.ml" append.

> Given that Coq also generates the .mli files, I do get the less general type as you wish:
>
>  $ coqtop
>  Welcome to Coq 8.4pl5 (February 2015)
>  Coq < Require Import String ExtrOcamlString.
>  Coq < Extraction "Append.ml" append;
>  Coq < ^\Quit
>  $ ocamlc Append.mli Append.ml
>  $ ocaml
>          OCaml version 4.01.0
>  # #load "Append.cmo";;
>  # open Append;;
>  # append;;
>  - : char list -> char list -> char list = <fun>
>