Stream: Coq users

Topic: Unqualified names and order of Imports


view this post on Zulip Pierre Rousselin (Oct 31 2023 at 09:13):

Sometimes the order of the Imports matters a lot (the latest Import takes precedence if there are conflicts between unqualified names). This makes things very hard to debug. Is there a Warning one can set to detect these situations?

view this post on Zulip Pierre Roux (Oct 31 2023 at 10:23):

No warning but maybe some good practices:

view this post on Zulip Karl Palmskog (Oct 31 2023 at 10:29):

I also think library authors should provide explicit recommended "export files" that Require Export all reasonable things in the right order. The canonical example is all_ssreflect (and friends) in MathComp, and another example is Stdpp's prelude.

view this post on Zulip Karl Palmskog (Oct 31 2023 at 10:31):

... and users obviously need to know they should use these "export files" whenever possible


Last updated: Jun 23 2024 at 05:02 UTC