Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ltac and constr arguments with holes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac and constr arguments with holes


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Ltac and constr arguments with holes
  • Date: Thu, 06 Nov 2014 21:54:20 -0500

On 11/06/2014 08:56 PM, Jonathan wrote:

Actually - it is possible (in the trunk) if one is willing to use a bit of a kludge involving refine, an evar, and eval:

Tactic Notation "my_destruct" uconstr(p) :=
let e := fresh in
refine (let e := p in _);
[shelve
|let v := eval hnf in e in
match goal with _ : context[?C] |- _ => unify v C; clear e; destruct C eqn:? end].

Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (1 + _).

-- Jonathan


Oh, sorry, that only handles patterns with a single hole. Simple fix to make it work for any number of holes:

Tactic Notation "my_destruct" uconstr(p) :=
let e := fresh in
refine (let e := p in _);
shelve_unifiable;
let v := eval hnf in e in
match goal with _ : context[?C] |- _ =>
unify v C; clear e; destruct C eqn:?
end.

Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (_ + _).

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page