Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ltac problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ltac problem


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Nuno Gaspar <nmpgaspar AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] ltac problem
  • Date: Fri, 16 Mar 2012 09:36:04 -0400

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).
(***)




Archive powered by MhonArc 2.6.16.

Top of Page