coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Warning, seemingly for no reason, is this a bug?

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Warning, seemingly for no reason, is this a bug?
Date: Sun, 31 Dec 2017 07:48:53 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f46.google.com
Ironport-phdr: 9a23:J7Y/2B2iTRa54J4WsmDT+DRfVm0co7zxezQtwd8Zse0WLfad9pjvdHbS+e9qxAeQG9mDsrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPfglEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95PWixBGIO8bpAPBPcPM+lCqon9vEYFoByiCgmsHuPvyyRIimXr0qIg1uQhChvK3AokH98Vv3TUqc/6NKYWUeyv0KbIyjDDYupQ1Dzg64bIaggsre+QUb90a8bcykkiGxnbglmNqoHpJTyY2+ULvmOG9eRvT/ivhHQiqwxpojig2MMsio7Ri4IQ0F/E9CF5zJ8yJd25VEJ3eNCkHZRRui2AOIt2RcQiQ25suCkk0LEJpZm7fC0SxJQmwR7QdeCHfpCW7h7/UOudOzR1iXJ/dL6hmhq/8lKsx+L9W8Ws1VZFtCtFkt3CtnAX0BzT79CKRed9/ke72DaPzBrf5fxeLkAxjqrXMZghwrorm5octETMBC72mEHsgKCKcUUk//Ck6/77bbX+up+cK4h0hxniPaQpg8yzGPg3MgwTX2eA4um8z73i/UjhQLpQlPE2k6/ZsIrbJcsBvKK5DRVVgc4f7EO0CC7j29AFlzFTJ1VcPRmDkoLBOlfUIfm+A+3p0Hq2lzI+7PDcP6apLpzINTCXm7f7fK0750dZ00w1yfhQ4ptVDvcKJ/elCRy5j8DREhJsa1/8+O3gEtgojo4=

Dear all,

In my coq project i am getting the warning

Warning: Collision between bound variables of name l0
[variable-collision,ltac]

The tactic that causes this warning is

change (invalidate_pointers_list n2 n1 l'
   :: (fix map (l0 : list (list statement)) : list (list statement) :=
         match l0 with
         | nil => nil
         | a :: t => invalidate_pointers_list n2 n1 a :: map t
         end) ll)
   with (map (invalidate_pointers_list n2 n1) (l' :: ll)).

I do not see anything that the variable l0 could be colliding with. Also, renaming the variable l0 into something else does not get rid of the warning message.

Is this warning a bug in coq?

Have a nice day,

Chris Dams

[Coq-Club] Warning, seemingly for no reason, is this a bug?, Chris Dams, 12/31/2017