The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello

I was surprised to find out that the following does not generate any errors:

Goal forall (X Y : Type) (s : X) (p : X -> Y), 
       (let x := s in p x) = (match s with x => p x end).
reflexivity. 

Printing reveals, that the match above is probably eliminated before type 
checking. Nevertheless I find it strange that this input syntax is allowed. 

Is this a bug or a feature? I suspect it has something to do with the match 
compilation.

-- 
Regards
Christian