The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

The code

Set Implicit Arguments.

Parameter bar : nat -> Type.

Let foo := bar.

Goal forall n, bar n.

  change (@bar ?m) with (@foo m).

works fine and behaves as expected.  However, the code 

Set Implicit Arguments.

Parameter bar : nat -> Type.

Let foo := bar.

Goal forall n, bar n.

  Ltac barfoo := change (@bar ?m) with (@foo m).

  barfoo.

errors with

Toplevel input, characters 67-68:

Error: The reference m was not found in the current environment.

on the Ltac definition.  What's going on?  (I'm using Coq 8.4beta2.)

Thanks.

-Jason