The Coq mailing list

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

On 19/08/2016 15:12, Robbert Krebbers 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.

> Why is one
> required to import anything of Program from the standard library to use
> the Program vernacular?

That is because the Program command inserts symbols from Program.Tactics
in the term under construction.

Best regards,

Guillaume