coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Rui Baptista <rpgcbaptista AT gmail.com>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Beginner problem writing tactic
- Date: Thu, 01 Aug 2013 20:19:35 -0400
On 08/01/2013 08:09 PM, Rui Baptista wrote:
But the tactic
progress repeat
match goal with
| [H1 : _ |- _] => progress (
apply (proj1 OJQZ) in H1 ||
(apply eq_sym in H1; apply (proj1 OJQZ) in H1; try apply eq_sym in H1))
| [|- _] => progress (
apply (proj2 OJQZ) ||
(apply eq_sym; apply (proj2 OJQZ); try apply eq_sym))
end.
is just the result of "unfolding" rw_aux OJQZ. Why does that one work, but not the other?
I've made the argument of OJQZ implicit just so I could feed it to proj1 and proj2.
When I run your tactic that fails, I literally see an error message saying that the parameter of [OJQZ] can't be inferred, so that seems pretty clearly to be the problem. The extra context of [apply] is sufficient to determine the parameter, perhaps because of some magic in the [apply] implementation that can only be achieved in OCaml, not in your own Ltac definitions.
- [Coq-Club] Beginner problem writing tactic, rpgcbaptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Rui Baptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Rui Baptista, 08/02/2013
- Re: [Coq-Club] Beginner problem writing tactic, Adam Chlipala, 08/02/2013
Archive powered by MHonArc 2.6.18.