The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Nuno Gaspar wrote:
> Ltac so H := solve [H].
>
> Lemma wtf:
>   false = true -> False.
> Proof.
>   intro. so congruence.  (*fails here*)
> Now, in the following I just define a tactic that would do exactly the 
> same, and yet, for some reason it fails.

That's a funny one.  My guess is the disparity arises from the fact that 
[congruence] is a built-in tactic, implemented in OCaml.  By way of 
evidence, consider this alternate script:

(***)
Ltac so H := solve [ H ].

Ltac congruence' := congruence.

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

And this version that uses a function:

(***)
Ltac so H := solve [ H tt ].

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