coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Bind argument of tactic notation to scope

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