The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Hi Beta,

I haven't investigated in detail but my guess is that the dB context is turned into a named context (because Ltac does not handle dB) and appended to the section context, so the x is renamed as x0. There cannot be two vars with the same name in a named context. If you do not open a section, x is declared as a global constant (Top.x) so the renaming is not necessary.

This is of course surprising, but hard to avoid, unless Ltac is deeply reworked.

Bruno.

---

De: "Beta Ziliani" <beta AT mpi-sws.org>
À: "Coq Club" <coq-club AT inria.fr>
Envoyé: Vendredi 3 Février 2017 13:56:49
Objet: [Coq-Club] Bug or feature?

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

​