Fabian Kunze (Nov 18 2020 at 09:10): 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?
Fabian Kunze (Nov 18 2020 at 09:12):(coq 8.12 and equations 1.2.3+8.12)
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?
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 )
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?
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.
Paolo Giarrusso (Nov 18 2020 at 13:00):I finished my thought in your second issue; you (and they) want Export Arguments.
Paolo Giarrusso (Nov 18 2020 at 13:02):and you’re also asking Equations to migrate to it.
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.
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: Apr 19 2024 at 11:02 UTC