The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

You can re-abstract over the equality, and apply eq_refl from outside
the pattern-matching.

  refine (match n as k return (k = n) -> k + 0 = n with
    | 0 => _
    | S n' => _
    end eq_refl).

On Sun, Apr 6, 2014 at 8:44 PM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 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?
>
> Thanks.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net