coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
Chronological Thread
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
- Date: Tue, 27 Jan 2015 11:40:24 -0500
On 01/26/2015 11:25 AM, Jonathan Leivent wrote:
Here's a much easier, more complete, and perhaps even semi-respectable approach.
A better version that can take a mix of bindings and holes:
Ltac eshape := repeat eapply exist_shape.
Ltac shape type tac :=
multimatch goal with
H:_ |- _ =>
let S:=constr:
($(refine (_ : type); shelve_unifiable; eshape; exact H)$) in
tac H S
end.
Tactic Notation "Shape" uconstr(type) tactic3(tac) :=
shape type tac.
Which makes this possible:
Shape (xsh x, x \/ x \/ _) (fun H S => ...).
-- Jonathan
- [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/27/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
Archive powered by MHonArc 2.6.18.