The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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
> 
> ​