The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/13/2014 11:56 AM, Jonathan wrote:
> There are probably other cases where in "tac1; tac2" one would desire 
> a single invocation of tac2 to act on all subgoals generated from tac1 
> instead of having a separate invocation of tac2 for each. Why not just 
> have a syntax for that?  Something like "tac1 > tac2" to suggest that 
> all subgoals of tac1 are gathered into one call of tac2?

I know that the standard way to think about Ltac is that it has a 
Prolog-like control flow.  It's been a while since I did anything in 
Prolog, so I don't know if there's any similar construct for goal 
"joining" in more recent Prolog, nor if there is any reason to have 
one.  However, this goal gathering/joining makes me think about dataflow 
programming more even than logic programming.  The unit of "data" that 
is flowing is a subgoal obligation.  Some operations create them, some 
consume them, some do both.

Maybe that suggests an alternative way to think about evars? Suppose 
there is a join operation on an evar that gathers together all subgoals 
that depend on that evar...

-- Jonathan