coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using lists in Tactic Notations

From: Jay Kruer <jay.kruer AT sifive.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Using lists in Tactic Notations
Date: Tue, 20 Aug 2019 11:06:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jay.kruer AT sifive.com; spf=Pass smtp.mailfrom=jay.kruer AT sifive.com; spf=None smtp.helo=postmaster AT mail-pg1-f175.google.com
Ironport-phdr: 9a23:hlMGuRei4Jjy3ZHZMqR6d6hklGMj4u6mDksu8pMizoh2WeGdxcu4Yx7h7PlgxGXEQZ/co6odzbaP6ea5BTVLuM/e+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8UbjpZuJqksxhfUoHZDZvhby35vKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zRh8dtjqxUvQihqgR/zYDKfY+bOvlwcazBct4BWWpNQtxcWzBdDo+gc4cCCfcKM+ZCr4n6olsDtR+wChOsBejyzzFInGL20rMg0+88FgzG3hYvHtIUvHTXttX1KbkdUfquwanTzDXDYfJW2Snj54TSbh8hpvSMUKt2fMHMykcvDxvIgkuMpYHhJT+Y1eQAv3KF4+Z9Ve+jkXMrpgNxrzS328sglJPFipwJxl3F7yl13pg5KcOiREN7Z9OvDYFeuDuAN4RsR8MvW2Fotzg+yr0BoZO7eTIFyJUjxxLGc/yHfJWE7gvtVOqMIzp1hGhpeL24hxa1/kigzvPzWtOo31ZNqypJitjMtnYT2BzP8sWLVOdx80O71TuM1w3f8P9ILV00mKbBNpIswL49moIWsUvZHy/2nEv2jLWRdkUh4uWo6f7oY7X8qp+fLY90lx/xMr41l8ykAOQ4PAkOX3aF9uimyLLj+kj5TK1QjvIqiqnZrIzaJcMDq6GlBA9Vy58v5Aq7Dze7y9sVhmIHLVJAeBKflYflIVDOIPbiDfe+mVugijlrx+qVdoHmV57KNz3IlKrrVbd78U9VjgQpnv5F4JcBKLgQaNHpR0Lr/IjaBw5/MBapzvzPE9Rz150TH2mIB/nKY+vprVaU67d3cKG3b4gPtWOlcql317vVlXY83GQlU+ys1JoTZmq/G608cV6Yb3vyj5EKFmJY51NiHtyvs0WLVHtoX1j3R7g1v2tpE4OoDJnOAIuqhe7ZhXrpLthtfmlDT2u0PzLoeoGDAalebSuTJop5nWVBW+H+Fsku0hahsAK8wL1ifLLZ

Hi coq-club,

I am trying to use the *_list feature of Tactic Notation to parameterize
my tactic over a list of identifiers to be unfolded before the meat of
the tactic is executed. I am unable to get the feature working and I've
minimized my problem with it to a small example:

Tactic Notation (at level 0) "myUnfold" "[" reference_list(wl) "]" :=
cbv delta [wl].

If I try using this tactic as follows on a goal containing some
references to definitions d1 and d2:

myUnfold [d1 d2].

I get the following error:

In nested Ltac calls to "myUnfold [ (ref_list) ]" and "cbv delta
[wl]", last call failed.
Ltac variable wl is bound to d1 d2 which cannot be coerced to an
evaluable reference.

Any ideas as to what I've done wrong here?
-j

[Coq-Club] Using lists in Tactic Notations, Jay Kruer, 08/20/2019
- Re: [Coq-Club] Using lists in Tactic Notations, Pierre Courtieu, 08/21/2019