The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

I opened https://github.com/coq/coq/issues/9462

Best,
Théo

Le dim. 3 févr. 2019 à 15:43, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 a écrit :
>
>
>
> Le jeu. 31 janv. 2019 à 01:10, Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
>  a écrit :
>>
>>
>>
>> On 29/1/19 3:41 am, Pierre Courtieu wrote:
>> > all:tac. applies the tac to all goals.
>> > Period.
>>
>> Well, IMRO this is pretty unsatisfactory.  Since the order of applying
>> tactics (or parts of them) to subgoals matters (as in the case, for
>> example, of instantiating existential variables) you are making it seem
>> that coq's design is so complicated that it is not worth while trying to
>> describe it.
>
>
> I don’t know. Maybe the order in which goals are treated should be 
> explicited in documentation. Or maybe not. If one wants to force a 
> particular ordering then it is possible by focusing.
>
>>
>> And there is certainly nothing in the documentation, as far as I can
>> see, to explain, or even to alert the user to the fact that
>> all : solve_eqs
>> when there are two subgoals, solves both, whereas
>> all : repeat solve_eqs
>> leaves one of them unsolved
>
>
> It is sais in documentation as far as I can tell: « applied to each goal 
> independently means that is equivalent to 1:repeat solve_eqs. 2:repeat 
> solve_eqs...
> But indeed we need a repeat with the interleaved semantics.
>
> Can you fill a big report about that please?
>
> Best regards
> Pierre
>>
>>
>> Cheers,
>>
>> Jeremy