Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Feb 24, 2016 at 03:58:38PM +0100, Ralf Jung wrote:
> > I see what you mean, but I discovered "tactic notations" way after this
> > API was designed.  I hope it is possible to register custom tactic
> > arguments, but I don't know how to do it. Help is welcome.
> 
> I don't know any more about the internals of the tactic engine than you
> do :-/ . And I am not sure if I want to, I heard stories that our minds
> may not be able to cope well with the chaos that unfolds when digging
> into this... ;-)

With some help from Pierre Marie, I managed to fix "ssrpattern" and
pushed a commit.

This now works:

  Tactic Notation "at" ssrpatternarg(p) tactic(t) := 
     ssrpattern p; let top := fresh in intro top;
     t top; try unfold top in * |- *; clear top.

  Goal forall x y, x + y = 4.
  intros.
  at [RHS] (fun selected => remember selected as E eqn:E_def).

I hope it helps,
-- 
Enrico Tassi