The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Qinxiang,

I suspect that what happens is not that "destruct" uses "my_destruct",
but that your notation breaks the parsing rule for "destruct ... eqn".

The grammar rule for "destruct ... eqn" uses a sequence of tokens
("eqn" then ":") to represent "eqn:" while the grammar rule for
"my_destruct" uses a single token where ":" is attached to "eqn". The
rule added for "my_destruct" has the side effect of declaring "eqn:"
as a new token. Then, when trying to parse "destruct ... eqn:...", the
parser sees one token "eqn:" and this is not any more the two distinct
tokens "eqn" and ":" that it expects to see to match the grammar rule
for "destruct".

Unfortunately, to know that, "Print Grammar tactic" (which shows only
the first level of the grammar) is not enough. As the situation is
currently, you have to look at the source file of the grammar of
tactics [1].

So, if you change your rule into:

  Tactic Notation "my_destruct" constr(t) "as" simple_intropattern(pat)
  "eqn" ":" simple_intropattern(Heq) :=
     _my_destruct t Heq pat.

I suspect that it shall not break "destruct ... eqn:" any
more. (Alternatively, you could also use "destruct ... eqn : ..." with
a space between "eqn" and ":" but I doubt that this is the solution
that you'd like most.)

Best regards,

Hugo Herbelin

[1] 
https://github.com/coq/coq/blob/ac2c4bc19afe7d68918cbc6f605a9bcfcdbf0f35/plugins/ltac/g_tactic.ml4#L480

On Fri, May 25, 2018 at 07:18:19PM -0400, Cao Qinxiang wrote:
> Dear all,
> 
> I try to build a "destruct" like tactic for my own type as follows:
> 
> 
>     Ltac _my_destruct t Heq pat := ...
> 
>     Tactic Notation "my_destruct" constr(t) "as" simple_intropattern(pat)
>     "eqn:" simple_intropattern(Heq) :=
>        _my_destruct t Heq pat.
>    
>     Tactic Notation "my_destruct" constr(t) "as" simple_intropattern(pat) :=
>       let Heq := fresh "H" in
>        _my_destruct t Heq pat.
> 
> 
> However, this tactic notation will conflict with Coq's default "destruct ...
> eqn:" tactic. In other words, even "my_destruct" is a different name with
> "destruct", Coq will try to interpret  "destruct t eqn:H" as my user-defined
> tactic notation and fail.
> 
> Is there any way to solve this problem?
> 
> 
> Thank you very much!
> 
> Qinxiang
>