The Coq mailing list

[Arthur Chargu�raud <arthur AT chargueraud.org>]

> Ltac so H := solve [H].
>
> Lemma wtf:
>   false = true -> False.
> Proof.
>   intro. so congruence.  (*fails here*)
>
> I do not understand why the above fails. Help please :)
Hi, I think it's a kind of scoping problem. I usually use "tactic notation" 
to avoid this issue:
-------
Tactic Notation "so" tactic(H) := solve [H].

Lemma wtf:
  false = true -> False.
Proof.
  intro. so congruence.
-------

Alternatively, you can you "ltac:()" to locally change the scope:
-------
Ltac so H := solve [H].

Lemma wtf:
  false = true -> False.
Proof.
  intro. so ltac:(congruence).
-------

Best,
Arthur