text.v

Parameter f: nat -> nat.

Ltac foo := match goal with
| |- context ctx [S ?n] => idtac n
end.

Lemma bar : 2 = 1 + 1.
Proof.
foo.
reflexivity.
Qed.

Lemma baz : exists n:nat, S n = S n.
Proof.
    foo. (* fails to match *)
Qed.