The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

That definitely looks like a bug.  Still, I think there's an easier way 
to implement the function that you seem to want to implement, and this 
way doesn't hit any noticeable bug.

Inductive type : Set :=
| int : type
| Cbool : type
| ref : type -> type.

Definition value_set (t : type) :=
  match t with
    | int => nat
    | Cbool => bool
    | ref _ => nat
  end.

Inductive test : forall t, value_set t -> Prop :=
| test1 : forall t, test (ref t) 3
| test2 : test Cbool true.

Definition test_not_int (H : test int 5) : False :=
  match H in test T _ return match T return Prop with
                               | int => False
                               | _ => True
                             end with
    | test1 _ => I
    | _ => I
  end.