The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I'm sorry to be the "RTFM Parrot," but I think my answer to your last 
question is also the right one in this case: you should read an 
introduction to programming with dependent types in Coq, rather than 
trying to reconstruct the details through experimentation.

On 04/06/2014 02:44 PM, Ömer Sinan Ağacan wrote:
> Let's say I have code like this:
>
>    refine (match n with
>      | 0 =>  _
>      | S n' =>  _
>      end).
>
> In proof mode, I was expecting to get `n = 0` while filling first
> underscore and `n = S n'` while filling second underscore, in fact I
> can't make any progress in my program without this equalities. But Coq
> doesn't give them to me as hypothesis. Why is this and what should I
> do to have that equalities in proof mode?
>