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))}.
> 
> Write CamlLight File "Mytype" [Mytype].
> 
> Error during interpretation of command:
> Write CamlLight File "Mytype" [Mytype].
> Somebody raised a Failure exception
> "not an ML type".

Here is a patch to apply to the V6.3 that solves the problem.
Unfortunately, a lot of other things have changed since the release of
the V6.3 and I cannot warranty that the patch will apply properly.
The patch must be applied to the file tactics/contrib/extraction/fwtoml.ml
If the patch does not apply, do the modification directly, following
the patch below. I can help you if necessary.

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

======================================================================
RCS file:
/net/pauillac/constr/ARCHIVE/CONSTR/V6/tactics/contrib/extraction/fwtoml.ml,v
retrieving revision 1.30
retrieving revision 1.31
diff -c -r1.30 -r1.31
*** fwtoml.ml   1999/08/06 20:49:20     1.30
--- fwtoml.ml   1999/10/06 09:05:54     1.31
***************
*** 161,168 ****
   * [mltype_of_constr dbenv c] translates the type expression c into
   * an ML type expression, in a de Bruijn environment dbenv. *)
  
! let rec mltype_of_constr dbenv c = match (strip_outer_cast c) with
!     DOP2(Prod,c1,DLAM(name,c2)) ->
                let avoid = List.map (function TYPEparam id -> id
                                             | TYPEname id -> id)
dbenv in
                let id = ren_type avoid name in
--- 161,171 ----
   * [mltype_of_constr dbenv c] translates the type expression c into
   * an ML type expression, in a de Bruijn environment dbenv. *)
  
! let rec mltype_of_constr dbenv c = match whd_beta c with
!   | DOP2 (Cast,c,_) ->
!       mltype_of_constr dbenv c
! 
!   | DOP2(Prod,c1,DLAM(name,c2)) ->
                let avoid = List.map (function TYPEparam id -> id
                                             | TYPEname id -> id)
dbenv in
                let id = ren_type avoid name in