The Coq mailing list

[Dan Synek <synek AT cs.ru.nl>]

So, there is no way to make an Ltac return an error message from within a
match. Is it not time to fix this? Maybe an explicit break statement or 
something.
The idtac solution I do not like, since I want an error mesage and not 
just a printed message  followed by an ununderstandable error message 
(from the users point of view).
Thanks anyway  Se'bastien
Dan

Sébastien Hinderer wrote:

> 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.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> .
>
>