The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Bonjour,

Is the following a bug, or is there some reason to not expect dependent
records to extract? Is there any way to get round this?

-----------------------------------------
Record Mytype : Set := mkType { n : nat ; m : (sig nat (ge n))}.

Write CamlLight File "Mytype" [Mytype].

Error during interpretation of command:
Write CamlLight File "Mytype" [Mytype].
Somebody raised a Failure exception
"not an ML type".
If this is in user-written tactic code, then it needs to be modified.
If this is in system code, then it needs to be reported.
-----------------------------------------

However, extraction works as expected with the likes of

Definition MyStype := (sigS nat ([n:nat](sig nat (ge n)))).

Ewen Denney