The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Tue, Feb 10, 2015 at 05:54:20PM +0100, Frederic Chyzak wrote:
> (* Just for reference: ssreflect does it with the three replacements. *)
> Require Import ssreflect.
> Lemma foo5 (a : nat) : (fun c : nat => c + a + a = 42) a.
> Proof.
> case: a.
> Abort.

As already pointed out in this thread, chainging the goals into

  (fun selected => ...) item

to select some occurrences of item in the goal is the API used by
the pattern tactic to tell the tactic immediately following which
occurrences had to be operated on.

Since each ssreflect tactic offers good means to select occurrences, it
does not respect this API.  The default is to select all occurrences.

Best,
-- 
Enrico Tassi