The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

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