The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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>