The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I took a look at the ssr sources to see how the rewrite tactic is added 
to the Coq grammar:

  TACTIC EXTEND ssrrewrite
    | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] ->
    [ Proofview.V82.tactic (tclCLAUSES ist (ssrrewritetac ist args) 
clauses) ]
  END

I tried to mimic this using a tactic notation:

  Tactic Notation "foo" ssrrwargs(args) ssrclauses(clauses) :=
    rewrite args clauses.

Unfortunately, this does not work (see below for an example). Does 
anyone know a way of making this work?

----

From Coq.ssr Require Import ssreflect.
From Coq Require Import Arith.

Tactic Notation "foo" ssrrwargs(args) ssrclauses(clauses) :=
  rewrite args clauses.

Lemma test x y : x + y = y + x.
Fail foo /=.
Fail foo plus_comm.
(* Variable args should be bound to a term but is bound to a list. *)


On 01/01/2018 03:51 AM, Robbert Krebbers wrote:
> Hi Coq-club,
>
> I am trying to do something like:
>
>    Tactic Notation "foo" ssrrewriteargs(args) :=
>      do stuff;
>      rewrite args.
>
> So that for args I can take anything that the ssreflect rewrite tactic 
> accepts, e.g. `lem1 /= lem2 /const //`.
>
> Does anyone know if this is possible and what I should pick for 
> `ssrrewriteargs`?
>
> Thanks!
>
> Robbert