The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

I found what seems to me a weird behavior. Consider the following scenario:

Lemma yup:

  false = true -> False.

Proof.

  intro. solve [congruence].

Qed.

As expected, it succeeds proving. Now, in the following I just define a tactic that would do exactly the same, and yet, for some reason it fails.

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 :)

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.