The Coq mailing list

[Eric Jaeger <eric.jaeger AT ssi.gouv.fr>]

Hi all,

Just a short remark : the definition "Inductive Empty:Set:=." is
translated (versions 8.1 and 8.2) into Ocaml as "type empty=unit", which
does not appear to be the best possible translation today.

As far as I know, it is possible to declare an abstract type in Ocaml by
"type empty;;" - or, according to the revised syntax (not working on my
oooold ocaml version) "type empty='a;;".

Should one of these be used instead of the current translation ?

  Regards, Eric