coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic Notation conflict with default tactic

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Tactic Notation conflict with default tactic
Date: Fri, 25 May 2018 19:18:19 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
Ironport-phdr: 9a23:3vVMgRKdB2HBOMXtttmcpTZWNBhigK39O0sv0rFitYgQIvTxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicJOTA67W/ZlNB/gblBrx69vRFy2ZLYbJ2XOfd4Y6jTfckaRW1EXstJSSFOGIS8ZJYUAeoAO+ZZoIj9qEEIrRuxGAKhA//gxSVPhn/v3K061esgEQDc0wwmENIDq3vUrNDvO6cTVeC51rXHzTLGb/5P3zr29YvGcgg5rPyOUr98a9fdxVcvGg/fjVict5bpMjOa2+kLrmOV9fBvVfi1hG4iswxxoiagxsMrioTRg4Ia0FHE9SFgzIc7IN20VFd3YdCkHZZfrS2aOIx2QsQtQ2Fspik20KEJuZm+fCQSyZQnwQDQa+CffoWK7R/vTvudLSl4iX5/e7+zmQy+/Eivx+HkU8m7yldKri5LktnWsXAN0gTe5dSdRft650eh2DCP1g/S6u5eJ0A0mrHWK5EkwrEql5oTtV7PETPxmEXzlKOWbFkr+vC06+T7ZbXrvoOTN4htig3nLqsuntG/Dv8jPwgVX2mb/Py826f58U34RrVKlPw2nbPDvJDUP8RI7pK+VgRSy8Mo7wu1JzagytUR23cdf3xffxfSpIHuc2jPJuD5BPGwywCnmTByxvbWP7TnDb3CK3HClPHqerMruB0U8xY60d0Kv8EcMboGOv+mAhag5uydNQcwNkmP+8iiDdx80o0EXmfWW/2WNarTtRmD4ed9erDQNr9Qgy70Lr0e39CrlWUwwAZPcqyg3J9RY3e9TKw/fhepJEH0i9JEKl8k+wozSOuw1Q+HWD9XImm3B+cyu219B4WhAoPOAIuqhe7Z0Q==

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

[Coq-Club] Tactic Notation conflict with default tactic, Cao Qinxiang, 05/26/2018
- Re: [Coq-Club] Tactic Notation conflict with default tactic, Hugo Herbelin, 05/26/2018
  - Re: [Coq-Club] Tactic Notation conflict with default tactic, Cao Qinxiang, 05/26/2018