Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.5 extractor bug

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.5 extractor bug


Chronological Thread 
  • From: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq 8.5 extractor bug
  • Date: Tue, 9 Feb 2016 14:05:44 +0100

Hello,

You should post a bug report in the bug tracker:

https://coq.inria.fr/bugs/

Thanks,
--
JH Jourdan


Le 09/02/2016 12:11, Kazuhiko Sakaguchi a écrit :
> Hello,
>
> I found an extracted code that can't be typed in OCaml and Haskell.
> This issue happens on Coq 8.5, however, it can't be reproduced in Coq
> 8.5 beta 3.
>
> For more details, please see attached file.
>
> Thanks,
>
> Kazuhiko


Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page