Stream: Equations devs & users

Topic: eq_refl arguments in Equations.Prop


view this post on Zulip Fabian Kunze (Nov 18 2020 at 09:10):

I have a file F that transitively Require Imports another file G, which Require Imports Equations.Prop.
Is it a bug of Coq that in F, the implicit Argumentsof eq_refl are not the same before and after Importing G?

view this post on Zulip Fabian Kunze (Nov 18 2020 at 09:12):

(coq 8.12 and equations 1.2.3+8.12)

view this post on Zulip Fabian Kunze (Nov 18 2020 at 09:15):

I rephrase my question: Is this a known bug or should i investige this further and open an issue?

view this post on Zulip Fabian Kunze (Nov 18 2020 at 09:16):

Oh, ok... https://github.com/coq/coq/issues/9902 (EDIT: more likely https://github.com/coq/coq/issues/7654 )

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 12:49):

who changes eq_refl’s arguments, G or Equations? I guess your point is that it’s Equations?

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 12:50):

(Global) Hint Resolve has similar problems — it propagates on Require, not Import; for Coq 8.12, you can use Export Hint Resolve and have it propagate only when imported.

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 13:00):

I finished my thought in your second issue; you (and they) want Export Arguments.

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 13:02):

and you’re also asking Equations to migrate to it.

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 13:04):

I often end up with one or more prelude files that imports sets of dependencies and reset any global settings as needed — e.g. I load libraries A and B, which both change Obligation Tactic, then I set it again — so that everybody importing the prelude gets what the prelude sets, instead of throwing a coin through imports.

view this post on Zulip Fabian Kunze (Nov 18 2020 at 13:53):

Yes, Equation.Prop.Init changes eq_refl's implicit arguments, so it's a problem with equations, right.


Last updated: Jan 29 2023 at 16:02 UTC