The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.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
> )

The reference manual says:

  "fail n message": The number n is the failure level. If no level is
specified, it defaults to 0. (...) If non zero, the current match goal
block or try command is aborted and the level is decremented.

so that 

  match goal with
     | _ => fail 1 "error message"
  end.

should have worked. However it seems that this feature has never been
active, so that you have to download a recent cvs version (main branch
or V8-0-bugfix tag) to have fail working as specified. Sorry about
that.

  Best regards,

  Hugo