The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le lun. 28 janv. 2019 à 14:33, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> OK, so I'm understanding that all:tac is a tactic which does a bit of
> tac on each goal, then a bit more of tac on each goal, and so forth, is
> that correct?

That is not how I see things. all:tac. applies the tac to all goals.
Period. Just don't consider ";" as a way to combine "single goal"
tactics.


> If so then how do I find out or work out what the relevant bits of tac
> are? (eg, if tac is actually repeat tac')

Indeed the status of repeat is strange, but conforms to the documentation:

doc says:
"repeat expr:    expr is evaluated to v. If v denotes a tactic, this
tactic is applied to each focused goal *independently*."

so yes repeat is not a multigoal tactical. Which is strange.


Ltac prg a := let t := type of a in idtac t;(intro + now auto).

Goal (forall a b c d e f:bool, False) /\ (forall a y z t u v:nat, False).
Proof.
  split;intro.
  prg a; prg a ; prg a ; prg a ; prg a. (* nat boobl nat bool ...*)
  Undo.
  do 5 (prg a).  (* same *)
  Undo.
  do 2 (prg a;prg a). (* same *)
  Undo.
  repeat ltac:(prg a).  (* nat nat ... bool bool ...*)
  Undo.
  [> prg a; [> prg a ; [> prg a ; [> prg a ; [> prg a .. ].. ].. ].. ]
..  ]. (* same *)

It is indeed strnage that repeat is no a multigoal tactical whereas "do" is.

Is it possible to define multigoal tactics in ltac?

Pierre