The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Marko Malikoviæ wrote:
> Coq < Definition funkcija (x y : nat) : Prop :=
> Coq <   match x<y with
> Coq <       True => z=5
> Coq <     | _    => z=10
> Coq <   end.
> Warning: pattern True is understood as a pattern variable
> Toplevel input, characters 84-96
>   

The warning is very helpful in this case.  [True] is interpreted as a 
pattern variable, just like you had typed, e.g., [x] instead.  [True] is 
a type, not a constructor, so it isn't treated like, e.g., [true], which 
is a constructor of [bool].  You probably meant to use [bool] to start 
with and just miscapitalized the identifier, but [true] would also be a 
bug.  [x < y] is a logical proposition, not a value of an inductive 
type, so you will never be able to pattern match over it effectively in 
Gallina.  If you could figure out how to get Coq to decide the truth of 
arbitrary propositions like this, then you'd have solved the halting 
problem and more! :-)