The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/25/2015 05:42 PM, Jonathan Leivent wrote:
> shape rewrite (f ?[E] = g ?E)

To simplify: wrap the refine and unify work in a "test" tactic so that 
they are undone even if successful - hence no fear of leaking evars or 
unintentionally solving them.  After all, we only care to know whether 
the match worked or not, and are not in this case extracting out the 
terms that the evars unified with for use.

However, if no test tactic is used, it might be possible to extract the 
evar bindings in the tactic to run when the shape matches, which gets 
even more of the functionality of match.  Although how would one express 
that?  Maybe something like:

  shape (f ?[E1] ?[E2] = g ?E2 ?E1) tac (?E1, ?E2).

Hmmm... Maybe the real answer is to have an interactive-capable macro 
preprocessor that can sub "match goal with X |- _ => Y end" for 
"shape(X, Y)".  Do interactive-capable macro preprocessors exist?

-- Jonathan