The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

I confirm, there is currently a mess in the extraction of stdlib's Vector.t.
VectorDef.t and Vector.t aren't seen as equal as they should be (since
Vector.v contains an Include of VectorDef), leading to your two distinct
types t1 and t2. Probably that the Include of module-as-v-file isn't
well supported by extraction, unlike inner modules (Module...End inside
a .v file). I'll let you know when that's fixed.

Sorry for the inconvenience...
Pierre Letouzey

PS: for this kind of report, please favor the coq bugtracker instead
of plain mail to coq-club

----- Mail original -----
> Hello.
> 
> I have uploaded my code to github, see
> 
> https://github.com/dasuxullebt/deflate
> 
> In the main file "deflate.v", I try to extract several things. The
> extraction of quicksort_nat works. The extraction of fc1 fails somehow:
> 
> The type of lists is extracted twice, as "t0" and "t1". If I replace t1
> with t0 everywhere in the extracted code, then the code segfaults. A
> minimal reduction of the part that fails is:
> 
> let __ = let rec f _ = Obj.repr f in Obj.repr f;;
> type ('a, 'b) sum =
> | Inl of 'a
> | Inr of 'b;;
> type sumbool =
> | Left
> | Right;;
> match Obj.magic __ with
> | Inl x -> Left
> | Inr x -> Right;;
> 
> The proofs all should work in the current git-version (at least the
> version from 1 week ago). Do you have any clue of what is going wrong?
> 
> Best Regards,
> Christoph-Simon Senjak
>