Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

> Again, I did not play much with it, but I'd do a
> 
>   ssrpattern [pat]; intro selected; foo_tac selected; unfold selected; 
> clear selected

Oh, right, I can just use the Coq context. However, this still does not
work - at least when combined with "open_constr" tactic notation: It
seems to create shelved goals instead of actually unifying anything.

Tactic Notation "ssrpat" open_constr(pat) := ssrpattern [pat].
ssrpat (...). Unshelve.
<Goals appear for the holes in the pattern>

So, right now it does not seem possible to use ssrpattern in custom
tactics, only to use it directly in proof scripts. I tried to define an
"Ltac" instead of a "Tactic Notation", but was unable to get Coq to
accept that.

> 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... ;-)

> Internally patterns are represented as terms, but I'd try to avoid
> exploiting this fact ;-)

Indeed :D

Kind regards,
Ralf