The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to "split" evars in Coq?  I'm trying to get rewriting by shape to work (since it's my opinion that hypotheses should not have names).  I have a single rewrite working:

Ltac tac_shape shape tac :=

  match goal with

    | [ H : ?shape' |- _ ] => unify shape' shape; tac H

  end.

Tactic Notation "shape" "rewrite" open_constr(shape) := tac_shape shape ltac:(fun H => rewrite H).

Goal forall a b c d : Set, a = b -> b = c -> a = c.

  intros.

  repeat shape rewrite (_ = _); reflexivity.

But if I try to build an equivalent of [rewrite !H], and bring the [repeat] inside the tactic notation, then I end up with something that (predictably) doesn't work:

Ltac tac_shape shape tac :=

  match goal with

    | [ H : ?shape' |- _ ] => unify shape' shape; tac H

  end.

Tactic Notation "shape" "rewrite" open_constr(shape) := tac_shape shape ltac:(fun H => rewrite H).

Tactic Notation "shape" "rewrite" "?" open_constr(shape) := repeat tac_shape shape ltac:(fun H => rewrite !H).

Tactic Notation "shape" "rewrite" "!" open_constr(shape) := progress shape rewrite ? shape.

Goal forall a b c d : Set, a = b -> b = c -> a = c.

  intros.

  repeat shape rewrite (_ = _); reflexivity.

  Undo.

  shape rewrite ! (_ = _). reflexivity.

So my question is: is there a way to split the evars, so I can bring the [repeat] inside the [Tactic Notation] while keeping the pattern outside of it?

Thanks,

Jason