coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Bug or feature?

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Bug or feature?
Date: Fri, 3 Feb 2017 15:10:33 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:mzKxkRe775lQKvJhFUEoB7hXlGMj4u6mDksu8pMizoh2WeGdxc65YB7h7PlgxGXEQZ/co6odzbGH7+a/ACddsd7B6ClEK8McEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx/KN+cv3vrfabz9DmjbhKfMvdFTlmyyK6ZJT2dcqavtpi0jpq35odu1ayHlGJF+Xk17c68688YQryC9XofMn+IYAFPyiPvdwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09yCgzLpDPnWJi55innsOVV3TGbeNbpVvYzQzv0vPQjcwPhlCpSb21xy2rQkMEl3fpW

Hi,

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

Not just Ltac is affected by this kind of surprising renaming, see e.g.
<https://coq.inria.fr/bugs/show_bug.cgi?id=4536>.

Kind regards,
Ralf

[Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
- Re: [Coq-Club] Bug or feature?, Bruno Barras, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Ralf Jung, 02/03/2017
- Re: [Coq-Club] Bug or feature?, Maxime Dénès, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
    - Re: [Coq-Club] Bug or feature?, Andreas Abel, 02/05/2017
      - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/06/2017