The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Le 10/10/2018 à 16:43, Chris Dams a écrit :
> Dear all,
> 
> We all know the 'pattern' tactic but I was looking for something that
> takes multiple terms and does the same but came up empty. The idea is
> that we have, for instance the goal a + b = b + a and then can do
> 'patterns a b' to get the goal (fun a0 b0 : nat => a0 + b0 = b0 + a0) a
> b. Or have I missed something?

pattern a, b ?

D.