The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

Yes, there is a serious bug with Theorem with in 8.2-1. Sorry. The fix
will be released in the (next) "patch level" release of 8.2.

Hugo

From Chris Dams:
> The Theorem ... with ... construction seems nice too and is a reason
> to upgrade to 8.2, but does not work quite as well for me. If I do
> 
> Theorem mutual_ind_A:
>    forall P: A -> Prop,
>    forall Q: B -> Prop,
>    P mk_a ->
>    Q mk_b ->
>    (forall b: B, Q b -> P (S b)) ->
>    (forall a: A, P a -> Q (T a)) ->
>    forall a: A, P a
> with mutual_ind_B:
>    forall P: A -> Prop,
>    forall Q: B -> Prop,
>    P mk_a ->
>    Q mk_b ->
>    (forall b: B, Q b -> P (S b)) ->
>    (forall a: A, P a -> Q (T a)) ->
>    forall b: B, Q b.
> 
> Coq answers with "Anomaly: uncaught exception Not_found. Please report."