The Coq mailing list

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

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>
>