The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

I'm using Coq 8.3pl1, which I know is old.
I don't have a newer version handy to check on.
So, I'm posting this just-in-case.
This triggers the anomaly error message.


Require Import JMeq.

Inductive Even : nat -> Prop :=
| e0 : Even 0
| e2 : forall n, Even n -> Even (S (S n))
.

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.
*)

- -- 
echo 'scale=2735;sqrt(57)' | BC_LINE_LENGTH=391 bc |
tail -n 1 | tr 0-9 'ertiSSngl '
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAlChG2cACgkQxzVgPqtIcftZSQCfdE+8Spy1fMRvXrJ2x9wz/pU6
tYoAn3T99WK22rNxL7b4iWKIeL1GIV60
=WJxr
-----END PGP SIGNATURE-----