The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.