The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

> 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))}.

The extraction of Mytype is the following :

======================================================================
Coq < Extraction Mytype.
Mytype ==>
    Inductive Mytype : Set :=  mkType : nat->([P:Set]P nat)->Mytype
======================================================================

and, as you can notice, there is a redex, which is not an ML type
(there is no type operator in ML). If it was reduced, then the type
would be an ML type.

So, this is a bug, since types should be reduced before being
extracted, at least just before the ML extraction.

I send you a patch if I can find an easy solution to that problem.

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr