The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

assumption, as it happens, always has at most one success. In the current trunk, only the constructor tactic as well as the tactics which the user explicitly writes with + can have more than one success.

It doesn't matter how many ways the tactic could have succeeded, what matters is how many successes the tactic reports (they're computed lazily of course). For instance, the once tactical always reduces the number of successes to at most one, and as such, (exactly_once (once t)) is identical to (once t).

Multiple success tactics are new, so you may not expect many old tactics to have this behaviour (as it may break backward compatibility in a serious way). For instance, the "match goal/term" tactic _expression_ should naturally have multiple successes, but doesn't for compatibility (in fact, in the ml code there is a "once" inserted in the Ocaml code for precisely that reason (last line of interp_match_successes in tactics/tacinterp.ml).

I guess more multiple tactics will be coming (including a multiple-success match). But currently there are still few.

Best,

Arnaud

On 26 June 2014 02:47, Jonathan <jonikelee AT gmail.com> wrote:

From the documentation, I would have thought the following would fail:

Section X.
  Variable n : nat.
  Variable m : nat.
  Goal nat.
  Proof.
    exactly_once assumption.
  Qed.
End X.

If this is supposed to succeed, then what is meant by "at most one success" in the documentation for exactly_once?

-- Jonathan