The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Hi Dan,

> How do I rewrite this code so that the error message gets returned?
> Lemma F:False.
> match goal with
>   | _ => fail "error message"
> end.
> (It prints the following error message:
> User error: No matching clauses for match goal
> )
> thanks

To print an error message, you can use
idtac "Error!"
It is not very elegant but it's the only solution I know.
If I recall correctly, the problem with fail is that it makes the matching
fail, too. Then, due to Coq's backtracking features, the system looks for a
new pattern to match the goal. Since none is found, the message you gave is
displayed.
Using idtac should solve all this.

Hope this helps,
Sébastien.