The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think "[ > tac1; tac2; tac3 ]" is preferred when some tactics in the sequence "tac1; tac2; tac3" have multiple successes, but you can guarantee that all backtracking that needs to happen can happen within a single goal, rather than needing to backtrack across goal boundaries.

-Jason

On Jan 30, 2015 9:48 PM, "Jonathan Leivent" <jonikelee AT gmail.com> wrote:

When one has several backtracking-capable tactics with multiple successes - say tac1, tac2, and tac3 - when is it preferable to write "tac1; tac2; tac3" instead of "[> tac1; tac2; tac3 ..]"?

-- Jonathan

On 01/30/2015 06:41 PM, Jason Gross wrote:

Perhaps CHANGES should be updated to include [ > ... ] in it's replacement
for [constructor (tac)]?

-Jason
On Jan 30, 2015 4:29 PM, "Arnaud Spiwack" <aspiwack AT lix.polytechnique.fr>
wrote:

Well, as I've just wrote in the aforementioned tracker issue (#3969
<https://coq.inria.fr/bugs/show_bug.cgi?id=3969>), the solution is not
due to repeat. But to the goal-distribution tactic `[> t..]`. Indeed it's
important, here, to keep calls to `reflexivity` close to their
`constructor`: as Arthur wrote it, all the `constructor`s are called first,
then all the `reflexivity`-s and the search-space is just to big. So
`all:[> constructor;reflexivity ..]` will work as desired. If other tactics
are called later, it is probably wise to call `once [>
constructor;reflexivity ..]` because the tactics are not smart enough to
figure out that backtracking inside these calls to `constructor` is
pointless.