The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 19/08/2016 15:38, Robbert Krebbers wrote:
> On 08/19/2016 03:29 PM, Guillaume Melquiond wrote:
>>> > However, just importing Coq.Program.Syntax is enough.
>> This is kind of baffling: for some reason, requiring Program.Syntax
>> transitively causes Program.Tactics to be required.
> You are right. No idea where it comes from exactly.

It comes from the following dependency chain:

Program.Syntax
Lists.List
Setoids.Setoid
Classes.SetoidTactics
Program.Tactics

Best regards,

Guillaume