Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Errors in extracted program.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Errors in extracted program.


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page