The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
It seems reference_list is not what delta takes as argument. If this
is the case (experts will tell) this may deserve a feature wish/bug
report.

Meanwhile you can program something in ltac that is probably much less
efficient on big terms:

Require Import List.
Import List.ListNotations.

Ltac unf wl :=
  repeat progress (match wl with
                   | nil => idtac
                   | cons ?id ?wl' => cbv delta [id];unf wl'
                   end).
Goal forall x, x + x = 2 * x.
Proof.
  unf [Nat.add ; Nat.mul].

Hope this helps
Pierre

Le mer. 21 août 2019 à 07:54, Jay Kruer 
<jay.kruer AT sifive.com>
 a écrit :
>
> 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