The Coq mailing list

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

Hi,

> In the final Check command Coq says that the 3 in the first branch of
> the match is wrong (it is of course right about that!).
> It says:
> Error: In environment
> H2 : test int 5
> t''' : type
> The term "3" has type "nat" while it is expected to have type
>  "forall t'' : type, ref t'' = t'' -> False".
> 
> However, the type that Coq proposes is not right either!
> The pattern of this branch is test1 t''' and that is of type  test (ref 
> t''') 3.
> Hence in this case, to obtain the return type we should do the
> substitutions t' -> ref t''' and v'' -> 3.
> Hence the type that should be expected becomes
>      forall t'': type,
>      ref t''' = t'' ->
>      False
> However, Coq is requesting the type with t''' replaced with t''!

This is indeed a bug. Probably due to the same reason as bug 2193
(http://coq.inria.fr/bugs/show_bug.cgi?id=2193).

The development versions behave well but unfortunately not the
8.2pl1. Sorry.

Hugo Herbelin