The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

I just remembered: yesterday I submitted a bug report similar to this behavior.:

By defining the following tactic:

Ltac thus H :=
  solve[H].

And then trying it as follows:

Lemma test: forall n : nat, n <= n.
Proof.
  intro.
  thus firstorder.

It will yield an exception:

In nested Ltac calls to "thus", "H" (bound to
firstorder  (* Generic printer *)) and "firstorder  (* Generic printer *)",
last call failed.
Anomaly: uncaught exception Failure "Tactic extension: cannot occur".
Please report.

It does work however, by using "thus auto" instead of "thus firstorder".

2012/3/16 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).
(***)

--
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.