The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

  Here is the story.

> There was indeed some problem with the semantics of "match ... term"
> and "fail i" in Ltac.

  The execution of "fail n" was indeed broken in the released versions
8.0 and 8.0pl1 (it behaved like "fail 0", i.e. "fail" !).

  It has been fixed 2 monthes ago in the V8-0-bugfix cvs branch, which,
as the name says, is the branch which fixes (easily) fixable bugs of
Coq 8.0 without introducing new features.

  Unfortunately, fixing this bug revealed that the S_to_plus_simpl
example from the Coq'Art was in fact not compatible with the Reference
Manual. Indeed, the Reference Manual states that branches of a ltac
"match term with" are evaluated only after the "match" returns (thus
prohibiting jumping to the next pattern on tactic failure). To be
correct, the Coq'Art S_to_plus_simpl example should have used "fail 0".

  It has been decided that this lazy behaviour of ltac "match term
with" was non intuitive and that the next version (say Coq 8.1, which
has the "fail n" fixed too) will default to an eager version of ltac
"match term with" as it was in the first releases of the ltac
language. An extra keyword, still undecided, will be added though to
delay on demand the evaluation of tactics in clauses. With this new
behaviour, S_to_plus_simpl works unchanged in the current (non
V8-0-bugfix) cvs version.

  Since V8-0-bugfix is only intended to fix bugs, we didn't want to
change the behaviour of "match term with" in it. So we adopt a
pragmatic approach, which is still not exactly in conformity with the
Reference Manual but which at least does not break ltac code that
already worked in the 8.0 and 8.0pl1 versions (assuming this working
code did not use "fail n", which it must -- here is the point! --
since "fail n" was precisely broken) . Concretely, the pragmatic hack
was to say that "fail n", even if not evaluated within a "math term
with", was reduced to a "fail (n-1)" when seen outside the "match".
This hack has been implemented two weeks ago.

  To summarize, the Coq'Art has been incompatible with the cvs
8-0-bugfix version for one month and a half. The S_to_plus_simpl
example from the book still does not agree with the Reference Manual
but our analysis is, on this particular point, that the semantics
suggested by the book is better and that it will be adopted in the
next version 8.1 (and it is actually already adopted in our current
main cvs version).

  Hugo Herbelin