coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Errors in extracted program.
- Date: Wed, 02 Jul 2014 17:58:06 +0200
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
- [Coq-Club] Errors in extracted program., Christoph-Simon Senjak, 07/02/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/11/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/11/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/15/2014
- Re: [Coq-Club] Errors in extracted program., Christoph-Simon Senjak, 07/19/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/15/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/11/2014
- Re: [Coq-Club] Errors in extracted program., Pierre Letouzey, 07/11/2014
Archive powered by MHonArc 2.6.18.