coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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).
(***)
- [Coq-Club] ltac problem, Nuno Gaspar
- Re: [Coq-Club] ltac problem, Adam Chlipala
- Re: [Coq-Club] ltac problem, Nuno Gaspar
- Re: [Coq-Club] ltac problem,
Arthur Charguéraud
- Re: [Coq-Club] ltac problem, Hugo Herbelin
- Re: [Coq-Club] ltac problem, Adam Chlipala
Archive powered by MhonArc 2.6.16.