The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

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