The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Hi again,

Le 3 févr. 09 à 11:09, JAEGER, Eric (SGDN) a écrit :

> Yet I do not understand the behaviour of my_simpl2, 3 and 4 in  
> test'... How may I have different messages, one
> indicating success, the other failure? There is backtracking going  
> on here, but that does not give me any clue about what is happening.
>
> I hope to be clearer now ;-)

I think you are. It seems you are confused by the not-so-obvious  
semantics of [tac1 || tac2]
which differs from [first [ tac1 | tac2 ]] by backtracking when tac1  
fails _or_ does not
make progress.

Hope this helps,
-- Matthieu