The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Thanks Bruno and Maxime.

It is a bug then, although a tough one to fix, I suppose.

FWIW, In MetaCoq we used to have the de Bruijn context. Recently we decided to drop it and only use the named context; same as Ltac. But unlike Ltac, when we introduce the de Bruijn variables in the named context, we also rename the code, therefore changing x to x0 *inside the exact*, as should be done.

Best,

Beta

On Fri, Feb 3, 2017 at 10:18 AM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Beta,

I can't answer your question, since I'm not sure how much of Ltac's
binding is documented, but I can try to explain the symptom.

Since your binder clashes with the section variable name, the rooster
renames it on the fly. But then of course "x" designates the section
variable.

The following script should illustrate what goes on under the hood:

Section test.
Variable x : nat.
Definition ex := fun x y:nat=>ltac:(exact (x0 + y)).
Print ex.

Maxime.

On 02/03/17 13:56, Beta Ziliani wrote:
> Hi list,
>
> I stumble across what I think is an odd behavior when mixing named and
> dB contexts, and I’m going to file it as a bug unless someone convinces
> me that this is a feature:
>
> |Section test. Variable x : nat. Definition ex := fun x
> y:nat=>ltac:(exact (x + y)). Print ex. |
>
> outputs
>
> |ex = fun _ y : nat => x + y : nat -> nat -> nat |
>
> I am expecting, of course,
>
> |ex = fun x y : nat => x + y : nat -> nat -> nat |
>
> Note that defining `x` in a |Section| is important; if I make |x| a top
> level variable, the example is constructed as expected.
>
> Best,
> Beta
>
> ​