Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct

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




Archive powered by MHonArc 2.6.18.

Top of Page