coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq error

From: Pierre Letouzey <pierre.letouzey AT inria.fr>
To: S3 <scubed2 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq error
Date: Mon, 12 Nov 2012 17:48:08 +0100 (CET)

> Theorem split_e2 n0 n1 a b : n0 = n1 -> JMeq a b -> JMeq (e2 n0 a)
> (e2 n1 b).
> intros.
> induction H0.
> (*
> Anomaly: Uncaught exception Option.IsNone. Please report.
> *)
>

Hi

I confirm this anomaly is still there in all versions of Coq.
This issue looks a lot like an already existing bug report:

https://coq.inria.fr/bugs/show_bug.cgi?id=2814

Sorry for the annoyance...
Pierre L.

[Coq-Club] Coq error, S3, 11/12/2012
- Re: [Coq-Club] Coq error, Pierre Letouzey, 11/12/2012
- Re: [Coq-Club] Coq error, AUGER Cédric, 11/12/2012
  - Re: [Coq-Club] Coq error, S3, 11/13/2012