The Coq mailing list

[André Hirschowitz <ah AT unice.fr>]

> You loose pattern matching, but how can we define it?
>
> match z with
> | O => ...
> | S n => (any value is matched even O since S (S O)=O)
> end
You could write

Newmatch z with
| O => .A
| S n => B n
end

which should generate the single goal

Goal Oblig_O : B (S 0) =A.

ah