The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

The command "Extraction "file.ml" foo" (and variants thereof) also 
generates "file.mli" which contains the function signatures.

On 07/23/2015 07:37 PM, Éric Tanter wrote:
> Hi,
>
> Is it possible to instruct the extraction to ML to include type annotations 
> in function signatures?
>
> For instance, instead of producing this:
>
> (** val foo : int -> int **)
>
> let foo n = n + 1
>
> I would like the following:
>
> let foo (n:int) : int = n
>
> If not, how easy/hard/possible would it be to support it?
>
> Thanks!
>
> — Éric
>
> PS: yes, it *does* matter for the cases I’m considering ;-)