coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Bind argument of tactic notation to scope
- Date: Sat, 20 Feb 2016 16:39:41 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f50.google.com
- Ironport-phdr: 9a23:dQd/HheHfgaWuQNt0uCn2gbolGMj4u6mDksu8pMizoh2WeGdxc6+bR7h7PlgxGXEQZ/co6odzbGG7Oa9AydZvcnJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuOOU4R2GX1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/rJngsgCGRg+S7FMdVH8Xm1xGGV6Wwgv9W8LTuzD9sKJSwi6BJoWiT7kvXjKt9aBwU07AhyIONjp/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz
No, it's not. There's an open feature request at https://coq.inria.fr/bugs/show_bug.cgi?id=4381.
On Sat, Feb 20, 2016 at 3:41 PM, Ralf Jung <jung AT mpi-sws.org> wrote:
Hi all,
Is it somehow possible to bind the argument of a tactic notation to a
scope? I would like something similar to what we can do with
Arguments... _%S.
for functions and with
Notation "{[ e ]}" := (f e%S).
for normal notation. I tried this:
Tactic Notation "assume" constr(P) := cut (P%S).
but it does not seem to have any effect. See the attached file for an
example.
Kind regards,
Ralf
- [Coq-Club] Bind argument of tactic notation to scope, Ralf Jung, 02/20/2016
- Re: [Coq-Club] Bind argument of tactic notation to scope, Jason Gross, 02/20/2016
Archive powered by MHonArc 2.6.18.