The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 6 Apr 2014 21:44:13 +0300,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> 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

Something like:
   refine (match n as n' return n = n' -> _ with
     | 0 => _
     | S n' => _
     end (eq_refl n)).

Should do the trick (not tested, though). The usual tactic for that is
'case_eq'.