The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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